English
For i ∈ ι and m ∈ M, n ∈ N, the inverse image of Finsupp.single i (m ⊗ₜ n) is Finsupp.single i m ⊗ₜ Finsupp.single i n.
Русский
Для i ∈ ι, m ∈ M и n ∈ N, обратное отображение sends Finsupp.single i (m ⊗ n) в Finsupp.single i m ⊗ Finsupp.single i n.
LaTeX
$$$ (finsuppTensorFinsupp R S M N ι κ).symm (Finsupp.single i (m ⊗ₜ n)) = Finsupp.single i.1 m ⊗ₜ Finsupp.single i.2 n $$$
Lean4
@[simp]
theorem finsuppTensorFinsupp_symm_single (i : ι × κ) (m : M) (n : N) :
(finsuppTensorFinsupp R S M N ι κ).symm (Finsupp.single i (m ⊗ₜ n)) =
Finsupp.single i.1 m ⊗ₜ Finsupp.single i.2 n :=
Prod.casesOn i fun _ _ => (LinearEquiv.symm_apply_eq _).2 (finsuppTensorFinsupp_single _ _ _ _ _ _ _ _ _ _).symm