Commit 2025-06-09 04:25 9168cb3c

View on Github →

feat(GroupWithZero): monoid with zero homs to (co)products (#25466) Factored out from #22420

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/GroupWithZero/Hom.lean

added theorem MonoidWithZeroHom.one_apply_of_ne_zero

added theorem MonoidWithZeroHom.one_apply_zero

Modified Mathlib/Algebra/GroupWithZero/Prod.lean

added theorem WithZero.toMonoidWithZeroHom_withZeroUnitsEquiv

Created Mathlib/Algebra/GroupWithZero/ProdHom.lean

added theorem MonoidWithZeroHom.commute_inl_inr

added def MonoidWithZeroHom.fst

added theorem MonoidWithZeroHom.fst_apply_coe

added theorem MonoidWithZeroHom.fst_comp_inl

added theorem MonoidWithZeroHom.fst_comp_inr

added theorem MonoidWithZeroHom.fst_inl

added theorem MonoidWithZeroHom.fst_inr_apply_of_ne_zero

added theorem MonoidWithZeroHom.fst_surjective

added def MonoidWithZeroHom.inl

added theorem MonoidWithZeroHom.inl_apply_unit

added theorem MonoidWithZeroHom.inl_injective

added theorem MonoidWithZeroHom.inl_mul_inr_eq_mk_of_unit

added def MonoidWithZeroHom.inr

added theorem MonoidWithZeroHom.inr_apply_unit

added theorem MonoidWithZeroHom.inr_injective

added theorem MonoidWithZeroHom.one_apply_apply_eq

added theorem MonoidWithZeroHom.one_comp

added def MonoidWithZeroHom.snd

added theorem MonoidWithZeroHom.snd_apply_coe

added theorem MonoidWithZeroHom.snd_comp_inl

added theorem MonoidWithZeroHom.snd_comp_inr

added theorem MonoidWithZeroHom.snd_inl_apply_of_ne_zero

added theorem MonoidWithZeroHom.snd_inr

added theorem MonoidWithZeroHom.snd_surjective

Modified Mathlib/Algebra/GroupWithZero/Units/Lemmas.lean

modified theorem map_ne_zero

Modified Mathlib/Algebra/GroupWithZero/WithZero.lean

added theorem MonoidWithZeroHom.apply_one_apply_eq

added theorem MonoidWithZeroHom.comp_one

added theorem MonoidWithZeroHom.one_apply_val_unit

added theorem WithZero.recZeroCoe_one

added theorem WithZero.withZeroUnitsEquiv_symm_apply_coe