mathlib
ab1bf0fb - feat(algebra/order/monoid): add eq_one_or_one_lt (#13131)

Commit

3 years ago

feat(algebra/order/monoid): add eq_one_or_one_lt (#13131) Needed in LTE.

Author

kbuzzard

kbuzzard

Parents

Loading