Def MonoidHom.toHomUnitsMulEquiv

Modification history

2025-08-13 07:23

Mathlib/Algebra/Group/Units/Hom.lean

feat: `MonoidHom.toHomUnits` is a monoid hom (#27210) …

Added MonoidHom.toHomUnitsMulEquiv View on Github →