finsuppScalarLeft_apply — Mathlib

English

For pn ∈ (ι →₀ M) ⊗ N, the i-th coefficient of finsuppScalarLeft(pn) equals m_i times n with m_i coming from pn.

Русский

Для pn ∈ (ι →₀ M) ⊗ N коэффициент i в finsuppScalarLeft(pn) равен m_i n, где m_i — элемент pn в позиции i.

LaTeX

$$$ finsuppScalarLeft R N ι pn i = (Finsupp.lapply i) \\cdot pn $$$

Lean4

theorem finsuppScalarLeft_apply (pn : (ι →₀ R) ⊗[R] N) (i : ι) :
    finsuppScalarLeft R N ι pn i = TensorProduct.lid R N ((Finsupp.lapply i).rTensor N pn) := by
  simp [finsuppScalarLeft, finsuppLeft_apply]

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