finsuppScalarLeft_apply_tmul_apply

English

For p ∈ ι →₀ R and n ∈ N, the i-th coordinate of finsuppScalarLeft applied to p ⊗ n is p(i) · n.

Русский

Для p ∈ ι →₀ R и n ∈ N i-ая координата finsuppScalarLeft(p ⊗ n) равна p(i)·n.

LaTeX

$$$ finsuppScalarLeft R N ι (p \\otimes n) i = p(i) \\cdot n $$$

Lean4

@[simp]
theorem finsuppScalarLeft_apply_tmul_apply (p : ι →₀ R) (n : N) (i : ι) :
    finsuppScalarLeft R N ι (p ⊗ₜ[R] n) i = p i • n := by simp [finsuppScalarLeft]

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