primitive_element_iff_minpoly_degree_eq

English

Let F and E be fields with a finite set of intermediate fields; for any α ∈ E there exists β such that F⟮α⟯ ≃ K for some finite intermediate field K; i.e., there is a primitive element for finite intermediate fields.

Русский

Пусть между F и E конечное множество промежуточных полей; для каждого α ∈ E существует β так, что F⟮α⟯ является примитивным элементом над некоторым конечным промежуточным полем.

LaTeX

$$$\exists \alpha\in E,\ F\langle \alpha\rangle = K$ для некоторого конечного K, в частности существует примитивный элемент для конечных полей$$

Lean4

theorem primitive_element_iff_minpoly_degree_eq (α : E) : F⟮α⟯ = ⊤ ↔ (minpoly F α).degree = finrank F E :=
  by
  rw [degree_eq_iff_natDegree_eq, primitive_element_iff_minpoly_natDegree_eq]
  exact minpoly.ne_zero_of_finite F α

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