eq_of_root — Mathlib

English

Degree of minpoly is at most the dimension of the extension; i.e., deg(minpoly K x) ≤ finrank K L.

Русский

Степень minpoly не превосходит размерности расширения: deg(minpoly K x) ≤ finrank_K L.

LaTeX

$$$\deg(\minpoly K x) \le \operatorname{finrank}_K L$$$

Lean4

/-- If `y : L` is a root of `minpoly K x`, then `minpoly K y = minpoly K x`. -/
theorem eq_of_root {x y : L} (hx : IsAlgebraic K x) (h_ev : Polynomial.aeval y (minpoly K x) = 0) :
    minpoly K y = minpoly K x :=
  ((eq_iff_aeval_minpoly_eq_zero hx.isIntegral).mpr h_ev).symm

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