scalarRTensor_apply_tmul — Mathlib

English

For p ∈ MvPolynomial σ R and n ∈ N, scalarRTensor(p ⊗ n) equals p.sum (λ i m, Finsupp.single i (m ⊗ n)).

Русский

Для полинома p и элемента n образ scalarRTensor(p ⊗ n) равен сумме по мономам p с мономами Finsupp.

LaTeX

$$$scalarRTensor(p \\otimes n) = p.\\,sum(\\lambda i m.\\; Finsupp.single i (m \\otimes n))$$$

Lean4

theorem scalarRTensor_apply_tmul (p : MvPolynomial σ R) (n : N) :
    scalarRTensor (p ⊗ₜ[R] n) = p.sum (fun i m ↦ Finsupp.single i (m • n)) :=
  TensorProduct.finsuppScalarLeft_apply_tmul p n

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