Def WithZero.withZeroUnitsEquiv

Modification history

2024-09-14 07:51

Mathlib/Algebra/GroupWithZero/WithZero.lean

feat(Algebra/GroupWithZero): MulEquiv between WithZero (units) and the base group with zero (#16615) …

Added WithZero.withZeroUnitsEquiv View on Github →