aeval_eq_constantCoeff_of_vars — Mathlib

English

If in p.vars every i has g(i) = 0, then aeval g p equals algebraMap of the constant coefficient of p.

Русский

Если для каждого i в p.vars выполняется g(i) = 0, то aeval g p равно отображению алгебры от константного коэффициента p.

LaTeX

$$$ aeval\ g\ p = algebraMap\ _\ _ (constantCoeff\ p) $$$

Lean4

theorem aeval_eq_constantCoeff_of_vars [Algebra R S] {g : σ → S} {p : MvPolynomial σ R} (hp : ∀ i ∈ p.vars, g i = 0) :
    aeval g p = algebraMap _ _ (constantCoeff p) :=
  eval₂Hom_eq_constantCoeff_of_vars _ hp

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