Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-15 04:54 e86ab0b0

View on Github →

refactor(src/algebra/order/monoid): make bot_eq_zero a simp lemma only when the order is linear (#14553)

Estimated changes

Modified src/algebra/lie/subalgebra.lean

deleted def lie_subalgebra.canonically_ordered_add_monoid

Modified src/algebra/module/submodule/pointwise.lean

deleted def submodule.canonically_ordered_add_monoid

Modified src/algebra/order/monoid.lean

added theorem bot_eq_one'

modified theorem bot_eq_one

Modified src/data/multiset/basic.lean

added theorem multiset.bot_eq_zero