finsuppScalarLeft_symm_apply_single

English

The inverse of finsuppScalarLeft sends Finsupp.single i n to (Finsupp.single i 1) ⊗ n.

Русский

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

LaTeX

$$$ (finsuppScalarLeft R N ι).symm (Finsupp.single i n) = (Finsupp.single i 1) \\otimes_R n $$$

Lean4

@[simp]
theorem finsuppScalarLeft_symm_apply_single (i : ι) (n : N) :
    (finsuppScalarLeft R N ι).symm (Finsupp.single i n) = (Finsupp.single i 1) ⊗ₜ[R] n := by
  simp [finsuppScalarLeft, finsuppLeft_symm_apply_single]

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