eval₂_root — Mathlib

English

The polynomial f, when evaluated at the root of f inside AdjoinRoot f, vanishes; equivalently, the root is a root of the mapped polynomial f.

Русский

Полином f, будучи испытан на корне f внутри AdjoinRoot f, обращается в ноль; иначе говоря, корень является корнем отображенного полинома f.

LaTeX

$$$f(\\mathrm{root}(f)) = 0$ in \\operatorname{AdjoinRoot} f, i.e. \\; f\\,\\mathrm{eval}_{\\mathrm{root}(f)} = 0$$$

Lean4

@[simp]
theorem eval₂_root (f : R[X]) : f.eval₂ (of f) (root f) = 0 := by rw [← algebraMap_eq, ← aeval_def, aeval_eq, mk_self]

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