instDistribMulActionAddMonoidHom — Mathlib

English

There is a DistribMulAction DomMulAct M on the space of MonoidHom A B when B is CommMonoid and A is Monoid.

Русский

Существет DistribMulAction DomMulAct M на пространство MonoidHom A B, когда B является коммутативным моноидом, а A — моноид.

LaTeX

$$$\text{DistribMulAction } (DomMulAct M) (MonoidHom A B)$$$

Lean4

instance [Monoid M] [AddMonoid A] [DistribMulAction M A] [AddCommMonoid B] : DistribMulAction Mᵈᵐᵃ (A →+ B) :=
  DFunLike.coe_injective.distribMulAction (AddMonoidHom.coeFn A B) fun _ _ ↦ rfl

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