mulLeftMap_apply — Mathlib

English

Applying mulLeftMap to a singleton yields the corresponding scalar multiple of the left element.

Русский

Применение mulLeftMap к единичному элементу даёт соответствующее скалярное умножение левого элемента.

LaTeX

$$$mulLeftMap N m (\mathrm{single}\,i\,n) = (m i).1 * n.1$$$

Lean4

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

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