rTensor_apply_tmul — Mathlib

English

For p ∈ MvPolynomial σ S and n ∈ N, the image under rTensor of p ⊗ n is the sum over monomials of p, mapping each term to a basis element corresponding to that monomial’s index with coefficient m ⊗ n.

Русский

Для многочлена p и элемента n из N образ rTensor на p ⊗ n равен сумме по мономам p, где каждому моному ставится соответствующий элемент m ⊗ n.

LaTeX

$$$rTensor(p \\otimes n) = p.\\,sum(\\lambda i\\, m.\\; \\mathrm{Finsupp}.single\\, i\\, (m \\otimes n))$$$

Lean4

theorem rTensor_apply_tmul (p : MvPolynomial σ S) (n : N) :
    rTensor (p ⊗ₜ[R] n) = p.sum (fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n)) :=
  TensorProduct.finsuppLeft_apply_tmul p n

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