Open kckennylau opened 4 years ago
I've been trying to get linear_ordered_comm_group_with_zero
into mathlib. For that, I've
comm_group_with_zero
into mathlib,ordered_comm_monoid
was additive, and is now named ordered_add_comm_monoid
.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.
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
.