Def OrderMonoidIso.withZeroUnits
Modification history
2025-07-23 21:12
Mathlib/Algebra/Order/Hom/Monoid.lean
chore(Algebra/Order/Hom/Monoid): separate MonoidWithZero material into separate file (#27337) …
Modified OrderMonoidIso.withZeroUnitsView on Github →