monoid): add `with_zero.canonically_linear_ordered_add_monoid` (#12568)

Commit

3 years ago

feat(algebra/order/monoid): add `with_zero.canonically_linear_ordered_add_monoid` (#12568) This also removes some non-terminal `simp`s in nearby proofs

Author

eric-wieser

Parents

12786d04

mathlib e6fef397 - feat(algebra/order/monoid): add `with_zero.canonically_linear_ordered_add_monoid` (#12568)

mathlib
e6fef397 - feat(algebra/order/monoid): add `with_zero.canonically_linear_ordered_add_monoid` (#12568)