Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-30 14:01 ed6d94a8

View on Github →

chore(group_theory/group_action/defs): combine duplicated comp_hom and rename derivative definitions (#6942) Zulip thread

Estimated changes

Modified src/algebra/algebra/basic.lean

Modified src/algebra/module/basic.lean

deleted def ring_hom.comp_semimodule

added def semimodule.comp_hom

Modified src/algebra/smul_with_zero.lean

added def mul_action_with_zero.comp_hom

added def smul_with_zero.comp_hom

Modified src/group_theory/group_action/defs.lean

added def distrib_mul_action.comp_hom

deleted def monoid_hom.comp_distrib_mul_action

deleted def monoid_hom.comp_mul_action