finsuppTensorFinsupp'_symm_single_eq_single_one_tmul

English

The equality (finsuppTensorFinsupp'_symm_single_eq_single_one_tmul) states the inverse sends Finsupp.single (i) r to (Finsupp.single i.fst r) ⊗ (Finsupp.single i.snd 1).

Русский

Равенство: обратное отправляет Finsupp.single (i) r в Finsupp.single i.fst r ⊗ Finsupp.single i.snd 1.

LaTeX

$$$$ (\\mathrm{finsuppTensorFinsupp'}\\, R\\, \\iota\\, \\kappa)^{-1} (\\mathrm{Finsupp.single}\\ i\\ r) = \\mathrm{Finsupp.single}\\ i.1\\ r \\otimes \\mathrm{Finsupp.single}\\ i.2\\ 1. $$$$

Lean4

theorem finsuppTensorFinsupp'_symm_single_eq_single_one_tmul (i : ι × κ) (r : R) :
    (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i r) = Finsupp.single i.1 1 ⊗ₜ Finsupp.single i.2 r :=
  by
  nth_rw 1 [← one_mul r]
  exact finsuppTensorFinsupp'_symm_single_mul R ι κ i _ _

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