Commit 2025-08-13 07:23 dac1d0ca

View on Github →

feat: MonoidHom.toHomUnits is a monoid hom (#27210) From Toric

Estimated changes

Modified Mathlib/Algebra/Group/Units/Hom.lean

modified theorem MonoidHom.coe_toHomUnits

modified def MonoidHom.toHomUnits

added def MonoidHom.toHomUnitsMulEquiv

added theorem MonoidHom.toHomUnits_mul