finsuppTensorFinsupp'_symm_single_eq_tmul_single_one

English

The isomorphism finsuppTensorFinsuppRid R R ι κ coincides with finsuppTensorFinsupp' R ι κ.

Русский

Изоморфизм finsuppTensorFinsuppRid совпадает с finsuppTensorFinsupp'.

LaTeX

$$$$ finsuppTensorFinsuppRid\\ R\\ R\\ ι\\ κ = finsuppTensorFinsupp'\\ R\\ ι\\ κ. $$$$

Lean4

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

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