English
If a SMul-commuting class ensures compatibility, then a diagonal action translates to a distributive action on the Hom space.
Русский
Если класс SMul-коммутативности обеспечивает совместимость, то диагональное действие переходит в распределенное действие на пространстве гомоморфизмов.
LaTeX
$$$\text{SMulCommClass toDistribMulActionHom } \colon M\to A \to A$$$
Lean4
/-- If `DistribMulAction` of `M` and `N` on `A` commute,
then for each `c : M`, `(c • ·)` is an `N`-action additive homomorphism. -/
@[simps]
def _root_.SMulCommClass.toDistribMulActionHom {M} (N A : Type*) [Monoid N] [AddMonoid A] [DistribSMul M A]
[DistribMulAction N A] [SMulCommClass M N A] (c : M) : A →+[N] A :=
{ SMulCommClass.toMulActionHom N A c, DistribSMul.toAddMonoidHom _ c with toFun := (c • ·) }
