mathlib3
baefdf34 - fix(group_theory/group_action/defs): deduplicate `const_smul_hom` and `distrib_mul_action.to_add_monoid_hom` (#8953)

Commit
4 years ago
fix(group_theory/group_action/defs): deduplicate `const_smul_hom` and `distrib_mul_action.to_add_monoid_hom` (#8953) This removes `const_smul_hom` as `distrib_mul_action.to_add_monoid_hom` fits a larger family of similarly-named definitions. This also renames `distrib_mul_action.hom_add_monoid_hom` to `distrib_mul_action.to_add_monoid_End` to better match its statement. [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Definition.20elimination.20contest/near/237347199)
Author
Parents
Loading