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]