Theorems · Theorem · field theory

Field.exists_primitive_element_iff_finite_intermediateField

∀ (F : Type u_1) (E : Type u_2) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  (Algebra.IsAlgebraic F E ∧ ∃ α, F⟮α⟯ = ⊤) ↔ Finite (IntermediateField F E)

Steinitz theorem: an algebraic extension E of F has a primitive element (i.e. there is an α ∈ E such that F⟮α⟯ = (⊤ : Subalgebra F E)) if and only if there exist only finitely many intermediate fields between E and F.

Defined in

Mathlib.FieldTheory.PrimitiveElement

Cited by

0 results in Mathlib

Foundations

Depth 146 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldFieldAlgebra