finsuppLeft_apply — Mathlib

English

The finsuppLeft isomorphism applied to a general tensor t yields the rTensor with coordinates given by Finsupp.lapply.

Русский

Изоморфизм finsuppLeft, применённый к обобщённому тензору t, даёт rTensor с координатами, заданными Finsupp.lapply.

LaTeX

$$$finsuppLeft R M N ι t = rTensor N (Finsupp.lapply ι) t$$$

Lean4

theorem finsuppLeft_apply (t : (ι →₀ M) ⊗[R] N) (i : ι) : finsuppLeft R M N ι t i = rTensor N (Finsupp.lapply i) t := by
  induction t with
  | zero => simp
  | tmul f n => simp only [finsuppLeft_apply_tmul_apply, rTensor_tmul, Finsupp.lapply_apply]
  | add x y hx hy => simp [map_add, hx, hy]

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