Commit 2026-03-31 16:33 9799a649

View on Github →

feat(GroupTheory/GroupAction/Hom): connect existing definitions MulDistribMulActionHom and DistribMulActionHom using to_additive (#34249) In this PR, we defined MulDistribMulActionHom corresponding to DistribMulActionHom, which will be used in the multiplicative version of non-Abelian group cohomology.

Estimated changes

Modified Mathlib/Algebra/GroupWithZero/Action/Defs.lean

Modified Mathlib/GroupTheory/GroupAction/Hom.lean

added theorem DistriMulActionHom.coe_zero

added theorem DistriMulActionHom.zero_apply

deleted theorem DistribMulActionHom.coe_fn_coe'

deleted theorem DistribMulActionHom.coe_fn_coe

deleted theorem DistribMulActionHom.coe_one

deleted theorem DistribMulActionHom.coe_zero

modified def DistribMulActionHom.comp

deleted theorem DistribMulActionHom.comp_apply

deleted theorem DistribMulActionHom.comp_assoc

deleted theorem DistribMulActionHom.comp_id

deleted theorem DistribMulActionHom.ext

modified theorem DistribMulActionHom.ext_ring

deleted theorem DistribMulActionHom.id_apply

deleted theorem DistribMulActionHom.id_comp

modified def DistribMulActionHom.inverse

deleted theorem DistribMulActionHom.one_apply

deleted theorem DistribMulActionHom.toAddMonoidHom_injective

deleted theorem DistribMulActionHom.toFun_eq_coe

deleted theorem DistribMulActionHom.toMulActionHom_injective

deleted theorem DistribMulActionHom.zero_apply

modified structure DistribMulActionHom

added theorem MulDistribMulActionHom.coe_fn_coe'

added theorem MulDistribMulActionHom.coe_fn_coe

added theorem MulDistribMulActionHom.coe_one

added def MulDistribMulActionHom.comp

added theorem MulDistribMulActionHom.comp_apply

added theorem MulDistribMulActionHom.comp_assoc

added theorem MulDistribMulActionHom.comp_id

added theorem MulDistribMulActionHom.ext

added theorem MulDistribMulActionHom.id_apply

added theorem MulDistribMulActionHom.id_comp

added def MulDistribMulActionHom.inverse

added theorem MulDistribMulActionHom.one_apply

added theorem MulDistribMulActionHom.toFun_eq_coe

added theorem MulDistribMulActionHom.toMonoidHom_injective

added theorem MulDistribMulActionHom.toMulActionHom_injective

added structure MulDistribMulActionHom

added def MulDistribMulActionSemiHomClass.toMulDistribMulActionHom