mathlib
mathlib copied to clipboard
Published
20 hours ago •
leanprover-community
leanprover-community
chore(algebra/order/monoid_lemmas_zero_lt): remove useless lemmas, use namespace `without_zero_le_one`
The fourth part of #16449
There are still some useless lemmas that were simply ported from algebra/order/monoid_lemmas, this PR removes them.
Also, some lemmas have both assumptions like 1 < a 0 < a, this is because the file does not use type classes like zero_le_one_class currently. This PR puts these lemmas in the namespace without_zero_le_one.
