rTensor_apply_tmul_apply — Mathlib

English

For p ∈ MvPolynomial σ S, n ∈ N and d a finite-support function, the coordinate d of rTensor(p ⊗ n) equals coeff d p ⊗ n.

Русский

Координата d изображения rTensor(p ⊗ n) равна coeff d(p) ⊗ n.

LaTeX

$$$rTensor(p \\otimes n)\\,d = (coeff\\, d\\; p) \\otimes n$$$

Lean4

theorem rTensor_apply_tmul_apply (p : MvPolynomial σ S) (n : N) (d : σ →₀ ℕ) :
    rTensor (p ⊗ₜ[R] n) d = (coeff d p) ⊗ₜ[R] n :=
  TensorProduct.finsuppLeft_apply_tmul_apply p n d

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