aeval_def — Mathlib

English

For any p ∈ MvPolynomial σ R, the evaluation map aeval f coincides with the standard evaluation map evaluated via the underlying algebra map: aeval f p = eval₂Hom (algebraMap R S1) f p.

Русский

Для любого полинома p верно: aeval f p = eval₂Hom (algebraMap R S1) f p.

LaTeX

$$$\\\\mathrm{aeval} f \\\\; p = \\\\mathrm{eval}_{2\\mathrm{Hom}} (\\\\mathrm{algebraMap} R S_1) \\\\; f \\\\; p$$$

Lean4

theorem aeval_def (p : MvPolynomial σ R) : aeval f p = eval₂ (algebraMap R S₁) f p :=
  rfl

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