instMulActionAddMonoidHomOfDistribMulAction

English

There is a MulAction M^{dm} on AddMonoidHom A B with the standard action defined by c • f = f ∘ (mk.symm c ·).

Русский

Существует MulAction M^{dm} на AddMonoidHom A B с обычным действием: c • f = f ∘ mk.symm c · .

LaTeX

$$$\text{MulAction } (DomMulAct M) (AddMonoidHom A B)$ with $(c \cdot f)(a) = f(mk.symm c \cdot a)$$$

Lean4

instance [Monoid M] [AddMonoid A] [DistribMulAction M A] [AddZeroClass B] : MulAction Mᵈᵐᵃ (A →+ B) :=
  DFunLike.coe_injective.mulAction (⇑) fun _ _ ↦ rfl

Похожие утверждения