finsuppScalarRight_symm_apply_single

English

The map finsuppLeft' coincides with finsuppLeft on the underlying tensor product when varying the scalars.

Русский

Отображение finsuppLeft' совпадает с finsuppLeft на базовом тензорном произведении при изменении скаляров.

LaTeX

$$$ finsuppLeft'_apply R M N ι S x = finsuppLeft R M N ι x $$$

Lean4

@[simp]
theorem finsuppScalarRight_symm_apply_single (i : ι) (m : M) :
    (finsuppScalarRight R M ι).symm (Finsupp.single i m) = m ⊗ₜ[R] (Finsupp.single i 1) := by
  simp [finsuppScalarRight, finsuppRight_symm_apply_single]

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