Commit 2025-03-31 13:41 a68e6189

View on Github →

chore: make isUnit_iff_eq_one simp (#23484) This is very useful when talking about salient monoids (monoids whose only unit is 1). From Toric

Estimated changes

Modified Mathlib/Algebra/Group/Nat/Units.lean

Modified Mathlib/Algebra/Group/Units/Defs.lean

modified theorem isUnit_iff_eq_one

Modified Mathlib/RingTheory/Ideal/Operations.lean

Modified Mathlib/SetTheory/Cardinal/Divisibility.lean