finsuppRight_symm_apply_single — Mathlib

English

The inverse of finsuppRight sends Finsupp.single i (m ⊗ n) to m ⊗ Finsupp.single i n.

Русский

Обратное к finsuppRight отправляет Finsupp.single i (m ⊗ n) в m ⊗ Finsupp.single i n.

LaTeX

$$$ (finsuppRight R M N ι).symm (Finsupp.single i (m \\otimes_R n)) = m \\otimes_R Finsupp.single i n $$$

Lean4

@[simp]
theorem finsuppRight_symm_apply_single (i : ι) (m : M) (n : N) :
    (finsuppRight R M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) = m ⊗ₜ[R] Finsupp.single i n := by simp [finsuppRight]

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