Commit 2025-07-11 14:29 3e526e66

View on Github →

feat(Algebra/GroupWithZero): MulEquiv.toMonoidWithZeroHom (#26999) Helper projection to utilize MonoidWithZeroHomClass.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Equiv.lean

added def MulEquiv.toMonoidWithZeroHom

added theorem MulEquiv.toMonoidWithZeroHom_apply

added theorem MulEquiv.toMonoidWithZeroHom_bijective

added theorem MulEquiv.toMonoidWithZeroHom_inj

added theorem MulEquiv.toMonoidWithZeroHom_injective

added theorem MulEquiv.toMonoidWithZeroHom_surjective