eval₂_zero'_apply — Mathlib

English

The evaluation with zero on σ yields the base map on constants: eval₂ f (0) p = f(constantCoeff p).

Русский

Оценка с нулём на σ даёт основанное отображение на константах: eval₂ f (0) p = f(constantCoeff p).

LaTeX

$$$$ \mathrm{eval_2}\; f\; (0)\; p = f( \text{constantCoeff}(p) ) $$$$

Lean4

@[simp]
theorem eval₂_zero'_apply (f : R →+* S₂) (p : MvPolynomial σ R) :
    eval₂ f (fun _ => 0 : σ → S₂) p = f (constantCoeff p) :=
  eval₂_zero_apply f p

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