Commit 2023-01-16 10:37 07b3abc0

View on Github →

feat: port Algebra.Hom.GroupAction (#1424)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Hom/GroupAction.lean

added theorem DistribMulActionHom.coe_fn_coe'

added theorem DistribMulActionHom.coe_fn_coe

added theorem DistribMulActionHom.coe_one

added theorem DistribMulActionHom.coe_zero

added def DistribMulActionHom.comp

added theorem DistribMulActionHom.comp_apply

added theorem DistribMulActionHom.comp_id

added theorem DistribMulActionHom.ext

added theorem DistribMulActionHom.ext_iff

added theorem DistribMulActionHom.ext_ring

added theorem DistribMulActionHom.ext_ring_iff

added theorem DistribMulActionHom.id_apply

added theorem DistribMulActionHom.id_comp

added def DistribMulActionHom.inverse

added theorem DistribMulActionHom.one_apply

added theorem DistribMulActionHom.toAddMonoidHom_injective

added theorem DistribMulActionHom.toFun_eq_coe

added theorem DistribMulActionHom.toMulActionHom_injective

added theorem DistribMulActionHom.zero_apply

added structure DistribMulActionHom

added def DistribMulActionHomClass.toDistribMulActionHom

added def MulActionHom.comp

added theorem MulActionHom.comp_apply

added theorem MulActionHom.comp_id

added theorem MulActionHom.ext

added theorem MulActionHom.ext_iff

added theorem MulActionHom.id_apply

added theorem MulActionHom.id_comp

added def MulActionHom.inverse

added structure MulActionHom

added theorem MulSemiringActionHom.coe_fn_coe'

added theorem MulSemiringActionHom.coe_fn_coe

added def MulSemiringActionHom.comp

added theorem MulSemiringActionHom.comp_apply

added theorem MulSemiringActionHom.comp_id

added theorem MulSemiringActionHom.ext

added theorem MulSemiringActionHom.ext_iff

added theorem MulSemiringActionHom.id_apply

added theorem MulSemiringActionHom.id_comp

added structure MulSemiringActionHom

added def MulSemiringActionHomClass.toMulSemiringActionHom

added def SMulHomClass.toMulActionHom