Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-07 07:05 2a74d4e9

View on Github →

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

Estimated changes

added theorem eq_one_or_one_lt