English
The symmetric inverse of finsuppTensorFinsuppRid maps Finsupp.single i (r • n) to Finsupp.single i.1 r ⊗ Finsupp.single i.2 n where i ∈ ι × κ.
Русский
Обратное к симметричному отображению finsuppTensorFinsuppRid отправляет Finsupp.single i (r • n) в Finsupp.single i.1 r ⊗ Finsupp.single i.2 n, где i ∈ ι × κ.
LaTeX
$$$$ (\\mathrm{finsuppTensorFinsuppRid}\\, R\\, N\\, \\iota\\, \\kappa)^{-1} (\\mathrm{Finsupp.single}\\ i\\ (r \\cdot n)) = \\mathrm{Finsupp.single}\\ i.1\\ r \\otimes \\mathrm{Finsupp.single}\\ i.2\\ n. $$$$
Lean4
@[simp]
theorem finsuppTensorFinsuppRid_symm_single_smul (i : ι × κ) (m : M) (r : R) :
(finsuppTensorFinsuppRid R M ι κ).symm (Finsupp.single i (r • m)) = Finsupp.single i.1 m ⊗ₜ Finsupp.single i.2 r :=
Prod.casesOn i fun _ _ => (LinearEquiv.symm_apply_eq _).2 (finsuppTensorFinsuppRid_single_tmul_single ..).symm
