instDistribMulAction — Mathlib

English

There is a DistribMulAction instance on AddMonoidHom A B: M acts on A →+ B by pointwise action, given Monoid M and DistribMulAction M B.

Русский

Существует инстанс DistribMulAction на A →+ B: M действует на множество гомоморфизмов по точечному правилу, при заданном Monoid M и DistribMulAction M B.

LaTeX

$$[Monoid M] [DistribMulAction M B] : DistribMulAction M (A →+ B)$$

Lean4

instance [Monoid M] [DistribMulAction M B] : DistribMulAction M (A →+ B)
    where
  __ : DistribSMul _ _ := inferInstance
  one_smul _ := ext fun _ => one_smul _ _
  mul_smul _ _ _ := ext fun _ => mul_smul _ _ _

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