mulRightMap_apply — Mathlib

English

Similarly, mulRightMap distributes over finsupp sums by multiplying the right-hand factor with the left argument.

Русский

Аналогично, mulRightMap распределяет сумму finsupp, умножая правый фактор на левый аргумент.

LaTeX

$$mulRightMap M n m = Finsupp.sum m (\i x, x.1 * (n i).1)$$

Lean4

theorem mulRightMap_apply {M N : Submodule R S} {ι : Type*} (n : ι → N) (m : ι →₀ M) :
    mulRightMap M n m = Finsupp.sum m fun (i : ι) (m : M) ↦ m.1 * (n i).1 :=
  rfl

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