ofSubring — Mathlib

English

For x in integralClosure A L, the minimal polynomial over K of x equals the image of the minimal polynomial over A under the natural map.

Русский

Для x в интегральном замыкании A в L минимальный полином над K для x совпадает с образом минимального полинома над A по естественному отображению.

LaTeX

$$$\\minpoly K x = \\text{algebraMap} \\_{} (\\minpoly A x)$$$

Lean4

/-- The minimal polynomial of `x : L` over `K` agrees with its minimal polynomial over the
integrally closed subring `A`. -/
theorem ofSubring (x : integralClosure A L) : Polynomial.map (algebraMap A K) (minpoly A x) = minpoly K (x : L) :=
  eq_comm.mpr (isIntegrallyClosed_eq_field_fractions K L (IsIntegralClosure.isIntegral A L x))

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