finsuppTensorFinsupp'_symm_single_mul

English

The symmetric inverse of finsuppTensorFinsupp' sends Finsupp.single i r to Finsupp.single i.1 r ⊗ Finsupp.single i.2 1.

Русский

Обратное к симметричному отображению отправляет Finsupp.single i r в Finsupp.single i.1 r ⊗ Finsupp.single i.2 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_mul (i : ι × κ) (r₁ r₂ : R) :
    (finsuppTensorFinsupp' R ι κ).symm (Finsupp.single i (r₁ * r₂)) = Finsupp.single i.1 r₁ ⊗ₜ Finsupp.single i.2 r₂ :=
  finsuppTensorFinsuppLid_symm_single_smul R R ι κ i r₁ r₂

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