English
The symmetrized inverse of finsuppTensorFinsuppRid maps Finsupp.single i (r • n) to the tensor of the two singleton finsupps, i.e., Finsupp.single i.1 r ⊗ Finsupp.single i.2 n.
Русский
Обратное к изоморфизму finsuppTensorFinsuppRid отображает Finsupp.single i (r • n) в тензор двух единичных элементов: Finsupp.single i.1 r ⊗ Finsupp.single i.2 n.
LaTeX
$$$$ (\\mathrm{finsuppTensorFinsuppLid R N\\, \\iota\\, \\kappa})^{-1} \\bigl( \\mathrm{Finsupp.single}\\ i\\,(r \\cdot n) \\bigr) = \\mathrm{Finsupp.single}\\ i.1\\ r \\otimes \\mathrm{Finsupp.single}\\ i.2\\ n. $$$$
Lean4
@[simp]
theorem finsuppTensorFinsuppLid_symm_single_smul (i : ι × κ) (r : R) (n : N) :
(finsuppTensorFinsuppLid R N ι κ).symm (Finsupp.single i (r • n)) = Finsupp.single i.1 r ⊗ₜ Finsupp.single i.2 n :=
Prod.casesOn i fun _ _ => (LinearEquiv.symm_apply_eq _).2 (finsuppTensorFinsuppLid_single_tmul_single ..).symm
