Commit 2023-06-29 07:18 b0841bf5

View on Github →

feat: actions of DomMulAct on A →[N] B and A →+[N] B (#5378) Refs #5379

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Hom/GroupAction.lean

added def SMulCommClass.toDistribMulActionHom

added def SMulCommClass.toMulActionHom

Created Mathlib/GroupTheory/GroupAction/DomAct/ActionHom.lean

added theorem DomMulAct.mk_smul_mulActionHom_apply

added theorem DomMulAct.mk_smul_mulDistribActionHom_apply

added theorem DomMulAct.smul_mulActionHom_apply

added theorem DomMulAct.smul_mulDistribActionHom_apply

Modified Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean