Mathlib v3 is deprecated. Go to Mathlib v4

Theorem le_one_iff_eq_one

Modification history

2022-10-09 22:10

src/algebra/order/monoid.lean

chore(algebra/order/monoid): split into smaller files (#16861) …

Modified le_one_iff_eq_one View on Github →

2021-01-08 09:47

src/algebra/ordered_monoid.lean

chore(algebra/ordered_monoid): rename lemmas (#5657) …

Added le_one_iff_eq_one View on Github →