aeval_zero — Mathlib

English

Applying aeval with the zero function gives the base change of the constant term: aeval_0(p) = algebraMap(R → S1)(constantCoeff(p)).

Русский

Применение aeval к нулевой функции даёт отображение вдоль базы: aeval_0(p) = algebraMap(R → S1)(constantCoeff(p)).

LaTeX

$$$$ \mathrm{aeval}_{0}(p) = \mathrm{algebraMap}(R \to S_1)(\text{constantCoeff}(p)) $$$$

Lean4

@[simp]
theorem aeval_zero (p : MvPolynomial σ R) : aeval (0 : σ → S₁) p = algebraMap _ _ (constantCoeff p) :=
  eval₂Hom_zero_apply (algebraMap R S₁) p

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