aeval — Mathlib

English

For any x in B, aeval x (minpoly_A x) = 0; i.e., x is a root of its minimal polynomial.

Русский

Для любого x в B, aeval_x(minpoly_A x) = 0; то есть x является корнем своего минимального многочлена.

LaTeX

$$$\\operatorname{aeval}_{x}(\\minpoly_{A}(x)) = 0.$$$

Lean4

/-- An element is a root of its minimal polynomial. -/
@[simp]
theorem aeval : aeval x (minpoly A x) = 0 := by
  delta minpoly
  split_ifs with hx
  · exact (degree_lt_wf.min_mem _ hx).2
  · exact aeval_zero _

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