minpoly_gen — Mathlib

English

The minimal polynomial of α over F⟮α⟯ is the same as the minimal polynomial of α over F when considering the adjoined simple generator.

Русский

Минимальный многочлен элемента α над F⟮α⟯ совпадает с минимальным многочленом над F, при рассмотрении соответствующего простого порождающего элемента.

LaTeX

$$$\minpoly F(\AdjoinSimple.gen F α) = \minpoly F α$$$

Lean4

theorem minpoly_gen (α : E) : minpoly F (AdjoinSimple.gen F α) = minpoly F α := by
  rw [← minpoly.algebraMap_eq (algebraMap F⟮α⟯ E).injective, AdjoinSimple.algebraMap_gen]

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