Def MulEquiv.toMonoidWithZeroHom

Modification history

2026-06-06 05:44

Mathlib/Algebra/GroupWithZero/Equiv.lean

fix(RingTheory/Valuation): change `ValueGroup` from taking HomClass to Hom (#36911) …

Modified MulEquiv.toMonoidWithZeroHom View on Github →

2025-07-11 14:29

Mathlib/Algebra/GroupWithZero/Equiv.lean

feat(Algebra/GroupWithZero): `MulEquiv.toMonoidWithZeroHom` (#26999) …

Added MulEquiv.toMonoidWithZeroHom View on Github →