finsuppRight_apply — Mathlib

English

Every tensor t ∈ M ⊗ (ι →₀ N) maps under finsuppRight to a function whose i-th value is the induced tensor lTensor M (Finsupp.lapply i) t.

Русский

Каждый тензор t ∈ M ⊗ (ι →₀ N) отображается посредством finsuppRight в функцию, значение в i-го элемента есть тензор lTensor M (Finsupp.lapply i) t.

LaTeX

$$$ \\forall t \\in M \\otimes_R (\\iota \\to_0 N),\\ finsuppRight R M N ι t(i) = lTensor M (Finsupp.lapply i) t $$$

Lean4

theorem finsuppRight_apply (t : M ⊗[R] (ι →₀ N)) (i : ι) : finsuppRight R M N ι t i = lTensor M (Finsupp.lapply i) t :=
  by
  induction t with
  | zero => simp
  | tmul m f => simp [finsuppRight_apply_tmul_apply]
  | add x y hx hy => simp [map_add, hx, hy]

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