Commit 2024-09-14 07:51 f19f21c0

View on Github →

feat(Algebra/GroupWithZero): MulEquiv between WithZero (units) and the base group with zero (#16615) Also MulEquivs that add or remove WithZero on both sides And some basic WithOne/WithZero API

Estimated changes

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

added theorem WithOne.recOneCoe_coe

added theorem WithOne.recOneCoe_one

Modified Mathlib/Algebra/GroupWithZero/WithZero.lean

added def WithZero.withZeroUnitsEquiv