scalarRTensor_apply_tmul_apply — Mathlib

English

For p ∈ MvPolynomial σ R, n ∈ N, and d ∈ σ →₀ ℕ, the coordinate d of scalarRTensor(p ⊗ n) equals coeff d p · n.

Русский

Координата d образа scalarRTensor(p ⊗ n) равна coeff d p, умноженному на n.

LaTeX

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

Lean4

theorem scalarRTensor_apply_tmul_apply (p : MvPolynomial σ R) (n : N) (d : σ →₀ ℕ) :
    scalarRTensor (p ⊗ₜ[R] n) d = coeff d p • n :=
  TensorProduct.finsuppScalarLeft_apply_tmul_apply p n d

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