eval₂_zero_apply — Mathlib

English

The variant with a constant-zero function evaluated by f equals f(constantCoeff p).

Русский

Вариант с нулевой функцией константы: eval₂Hom f (fun _ => 0) p = f(constantCoeff p).

LaTeX

$$$$ \mathrm{eval_2Hom\_zero\'_apply}(f,p) = f( \text{constantCoeff}(p) ) $$$$

Lean4

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

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