instSMulOfDistribMulAction — Mathlib

English

There is a natural scalar multiplication action of a ring R on box-additive maps, compatible with distribution over addition.

Русский

Существует распределимое по умножению кольца R на BoxAdditiveMap, согласующееся с суммированием.

LaTeX

$$$\text{SMul of DistribMulAction } R (BoxAdditiveMap)\text{ instance}$$$

Lean4

instance {R} [Monoid R] [DistribMulAction R M] : SMul R (ι →ᵇᵃ[I₀] M) :=
  ⟨fun r f =>
    ⟨r • (f : Box ι → M), fun I hI π hπ => by simp only [Pi.smul_apply, ← smul_sum, sum_partition_boxes _ hI hπ]⟩⟩

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