aeval_eq_zero — Mathlib

English

If y is a conjugate root of x, then evaluating the minimal polynomial of x at y gives zero.

Русский

Если y сопряжён к x, то значение миниmального многочлена x в точке y равно нулю.

LaTeX

$$$a\\eval_y(\\minpoly(R, x)) = 0$$$

Lean4

/-- Let `p` be the minimal polynomial of `x`. If `y` is a conjugate root of `x`, then `p y = 0`.
-/
theorem aeval_eq_zero {x y : A} (h : IsConjRoot R x y) : aeval y (minpoly R x) = 0 :=
  h ▸ minpoly.aeval R y

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