finsuppTensorFinsupp_symm_single — Mathlib

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

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