Def WithZero.map'

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 WithZero.map'View on Github →