tensorModelOfHasCoeffsEquiv_tmul — Mathlib

English

Coefficients of relationOfHasCoeffs map to zero under evaluation by P.val.

Русский

Коэффициенты relationOfHasCoeffs переходят в ноль при оценке P.val.

LaTeX

$$$\\mathrm{MvPolynomial}.aeval\\ P.val\\ (\\mathrm{relationOfHasCoeffs}\\ R_0\\ r) = 0$$$

Lean4

@[simp]
theorem tensorModelOfHasCoeffsEquiv_tmul (x : R) (y : MvPolynomial ι R₀) :
    P.tensorModelOfHasCoeffsEquiv R₀ (x ⊗ₜ y) = algebraMap R S x * MvPolynomial.aeval P.val y :=
  rfl

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