minpoly_eq — Mathlib

English

For x ∈ S, the minimal polynomial of x over K inside S equals the minimal polynomial of x considered as an element of L.

Русский

Для x ∈ S минимальный многочлен над K внутри S равен минимальному многочлену x, рассматриваемому как элемент L.

LaTeX

$$$ \minpoly K x = \minpoly K (x : L) $$$

Lean4

theorem minpoly_eq (x : S) : minpoly K x = minpoly K (x : L) :=
  (minpoly.algebraMap_eq (algebraMap S L).injective x).symm

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