PR into mathlib

[kckennylau]

I believe one should PR the content of this repo into mathlib bit by bit to preserve this repo. Afterall, a Chinese proverb says that "anything not PR'ed into mathlib is lost in time".

I imagine this will start with src/for_mathlib.

[jcommelin]

I've been trying to get linear_ordered_comm_group_with_zero into mathlib. For that, I've

• PRd comm_group_with_zero into mathlib,
• moved large parts of the algebraic hierarchy from core into mathlib,
• mathlibs ordered_comm_monoid was additive, and is now named ordered_add_comm_monoid.
• We have [Merged by Bors] - refactor(algebra/ordered_group): multiplicative versions of ordered monoids/groups mathlib3#2844 to add the multiplicative counterparts...

After that, linear_ordered_comm_group_with_zero can be PRd. And the next step is valuation/basic.

So yes, I'm slowly trying to get things to mathlib.