Def MulEquiv.withZero

Modification history

2025-06-06 21:42

Mathlib/Algebra/GroupWithZero/WithZero.lean

feat(Algebra/Order/Hom/Monoid): order iso versions of unitsWithZero and friends (#22415)

Added MulEquiv.withZero View on Github →