English
Let R be a commutative semiring, M and N modules over R, and ι a finite index with decidable equality. The inverse of the canonical linear equivalence that reindexes tensors via Finsupp sends the simple tensor Finsupp.single i (m ⊗ n) back to (Finsupp.single i m) ⊗ n.
Русский
Пусть R — суждение коммутативного полугруппового кольца, M и N — модули над R, и ι — конечный индекс с существованием упорядочивания. Обратное отображение к каноническому линейному эквиваленту, переставляющему тензор, отправляет простой тензор Finsupp.single i (m ⊗ n) в Finsupp.single i m ⊗ n.
LaTeX
$$$ (\\text{finsuppLeft } R\, M\, N\, \\iota).\\mathrm{symm} (\\mathrm{Finsupp}.single\, i\\, (m \\otimes_{R} n)) = \\mathrm{Finsupp}.single\, i\, m \\otimes_{R} n $$$
Lean4
@[simp]
theorem finsuppLeft_symm_apply_single (i : ι) (m : M) (n : N) :
(finsuppLeft R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) = Finsupp.single i m ⊗ₜ[R] n := by simp [finsuppLeft]
