primitive_element_iff_minpoly_natDegree_eq

English

If F⟮α^m⟯ = F⟮α^n⟯ with m ≠ n, then α is algebraic over F.

Русский

Если F⟮α^m⟯ = F⟮α^n⟯ при m ≠ n, то α алгебраичен над F.

LaTeX

$$$m\neq n\Rightarrow F\langle \alpha^{m}\rangle = F\langle \alpha^{n}\rangle \Rightarrow \alpha\text{ is algebraic over }F$$$

Lean4

theorem primitive_element_iff_minpoly_natDegree_eq (α : E) : F⟮α⟯ = ⊤ ↔ (minpoly F α).natDegree = finrank F E :=
  by
  rw [← adjoin.finrank (IsIntegral.of_finite F α), ← finrank_top F E]
  refine ⟨fun h => ?_, fun h => eq_of_le_of_finrank_eq le_top h⟩
  exact congr_arg (fun K : IntermediateField F E => finrank F K) h

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