coe_aeval_eq_eval — Mathlib

English

For any p, aeval f p equals eval₂Hom (algebraMap R S1) f p. This states that the two ways of evaluating a polynomial coincide.

Русский

Для любого полинома 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

@[simp]
theorem coe_aeval_eq_eval : RingHomClass.toRingHom (MvPolynomial.aeval f) = MvPolynomial.eval f :=
  rfl

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