finsuppScalarRight_apply_tmul — Mathlib

English

For t ∈ M ⊗ (ι →₀ R) and i ∈ ι, the i-th component of finsuppScalarRight applied to t is the i-th coordinate computed by a rTensor map.

Русский

Для t ∈ M ⊗ (ι →₀ R) и i ∈ ι, i-я компонента finsuppScalarRight(t) вычисляется через rTensor по i.

LaTeX

$$$ finsuppScalarRight R M ι t i = TensorProduct.rid R M ((Finsupp.lapply i).lTensor M t) $$$

Lean4

theorem finsuppScalarRight_apply_tmul (m : M) (p : ι →₀ R) :
    finsuppScalarRight R M ι (m ⊗ₜ[R] p) = p.sum fun i n ↦ Finsupp.single i (n • m) :=
  by
  ext i
  rw [finsuppScalarRight_apply_tmul_apply, Finsupp.sum_apply,
    Finsupp.sum_eq_single i (fun _ _ ↦ Finsupp.single_eq_of_ne') (by simp), Finsupp.single_eq_same]

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