finsuppScalarRight_apply — Mathlib

English

For t ∈ M ⊗ (ι →₀ R), the i-th coordinate equals the image under lTensor of the i-th coordinate of the FinSupp argument.

Русский

Для t ∈ M ⊗ (ι →₀ R) i-ая координата равна изображению через lTensor от i-й координаты Finsupp.

LaTeX

$$$ t i = lTensor M (Finsupp.lapply i) t $$$

Lean4

theorem finsuppScalarRight_apply (t : M ⊗[R] (ι →₀ R)) (i : ι) :
    finsuppScalarRight R M ι t i = TensorProduct.rid R M ((Finsupp.lapply i).lTensor M t) := by
  simp [finsuppScalarRight, finsuppRight_apply]

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