Commit 2024-02-13 04:00 2524d76a

View on Github →

move: Move MonoidWithZeroHom to its own file (#10438) MonoidWithZeroHom confusingly pulled Algebra.GroupWithZero.Defs in Algebra.Group.Hom.Defs.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Free.lean

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

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

deleted theorem MonoidWithZeroHom.cancel_left

deleted theorem MonoidWithZeroHom.cancel_right

deleted theorem MonoidWithZeroHom.coe_coe

deleted theorem MonoidWithZeroHom.coe_comp

deleted theorem MonoidWithZeroHom.coe_copy

deleted theorem MonoidWithZeroHom.coe_inj

deleted theorem MonoidWithZeroHom.coe_mk

deleted def MonoidWithZeroHom.comp

deleted theorem MonoidWithZeroHom.comp_apply

deleted theorem MonoidWithZeroHom.comp_assoc

deleted theorem MonoidWithZeroHom.comp_id

deleted theorem MonoidWithZeroHom.congr_arg

deleted theorem MonoidWithZeroHom.congr_fun

deleted theorem MonoidWithZeroHom.copy_eq

deleted theorem MonoidWithZeroHom.ext

deleted theorem MonoidWithZeroHom.ext_iff

deleted def MonoidWithZeroHom.id

deleted theorem MonoidWithZeroHom.id_comp

deleted theorem MonoidWithZeroHom.mk_coe

deleted theorem MonoidWithZeroHom.toMonoidHom_coe

deleted theorem MonoidWithZeroHom.toMonoidHom_injective

deleted theorem MonoidWithZeroHom.toZeroHom_coe

deleted theorem MonoidWithZeroHom.toZeroHom_injective

deleted structure MonoidWithZeroHom

deleted def MonoidWithZeroHomClass.toMonoidWithZeroHom

Created Mathlib/Algebra/GroupWithZero/Hom.lean

added theorem MonoidWithZeroHom.cancel_left

added theorem MonoidWithZeroHom.cancel_right

added theorem MonoidWithZeroHom.coe_coe

added theorem MonoidWithZeroHom.coe_comp

added theorem MonoidWithZeroHom.coe_copy

added theorem MonoidWithZeroHom.coe_inj

added theorem MonoidWithZeroHom.coe_mk

added def MonoidWithZeroHom.comp

added theorem MonoidWithZeroHom.comp_apply

added theorem MonoidWithZeroHom.comp_assoc

added theorem MonoidWithZeroHom.comp_id

added theorem MonoidWithZeroHom.congr_arg

added theorem MonoidWithZeroHom.congr_fun

added theorem MonoidWithZeroHom.copy_eq

added theorem MonoidWithZeroHom.ext

added theorem MonoidWithZeroHom.ext_iff

added def MonoidWithZeroHom.id

added theorem MonoidWithZeroHom.id_comp

added theorem MonoidWithZeroHom.mk_coe

added theorem MonoidWithZeroHom.toMonoidHom_coe

added theorem MonoidWithZeroHom.toMonoidHom_injective

added theorem MonoidWithZeroHom.toZeroHom_coe

added theorem MonoidWithZeroHom.toZeroHom_injective

added structure MonoidWithZeroHom

added def MonoidWithZeroHomClass.toMonoidWithZeroHom

Modified Mathlib/Algebra/Ring/Hom/Defs.lean

Modified Mathlib/CategoryTheory/Groupoid/VertexGroup.lean