# Primitive Element Theorem #

In this file we prove the primitive element theorem.

## Main results #

• exists_primitive_element: a finite separable extension E / F has a primitive element, i.e. there is an α : E such that F⟮α⟯ = (⊤ : Subalgebra F E).

• exists_primitive_element_iff_finite_intermediateField: a finite extension E / F has a primitive element if and only if there exist only finitely many intermediate fields between E and F.

## Implementation notes #

In declaration names, primitive_element abbreviates adjoin_simple_eq_top: it stands for the statement F⟮α⟯ = (⊤ : Subalgebra F E). We did not add an extra declaration IsPrimitiveElement F α := F⟮α⟯ = (⊤ : Subalgebra F E) because this requires more unfolding without much obvious benefit.

## Tags #

### Primitive element theorem for finite fields #

theorem Field.exists_primitive_element_of_finite_top (F : Type u_1) [] (E : Type u_2) [] [Algebra F E] [] :
∃ (α : E), Fα =

Primitive element theorem assuming E is finite.

theorem Field.exists_primitive_element_of_finite_bot (F : Type u_1) [] (E : Type u_2) [] [Algebra F E] [] [] :
∃ (α : E), Fα =

Primitive element theorem for finite dimensional extension of a finite field.

### Primitive element theorem for infinite fields #

theorem Field.primitive_element_inf_aux_exists_c {F : Type u_1} [] [] {E : Type u_2} [] (ϕ : F →+* E) (α : E) (β : E) (f : ) (g : ) :
∃ (c : F), α'().roots, β'().roots, -(α' - α) / (β' - β) ϕ c
theorem Field.primitive_element_inf_aux (F : Type u_1) [] [] {E : Type u_2} [] (α : E) (β : E) [Algebra F E] [] :
∃ (γ : E), Fα, β = Fγ

This is the heart of the proof of the primitive element theorem. It shows that if F is infinite and α and β are separable over F then F⟮α, β⟯ is generated by a single element.

theorem Field.exists_primitive_element (F : Type u_1) (E : Type u_2) [] [] [Algebra F E] [] [] :
∃ (α : E), Fα =

Primitive element theorem: a finite separable field extension E of F has a primitive element, i.e. there is an α ∈ E such that F⟮α⟯ = (⊤ : Subalgebra F E).

noncomputable def Field.powerBasisOfFiniteOfSeparable (F : Type u_1) (E : Type u_2) [] [] [Algebra F E] [] [] :

Alternative phrasing of primitive element theorem: a finite separable field extension has a basis 1, α, α^2, ..., α^n.

See also exists_primitive_element.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Field.isAlgebraic_of_adjoin_eq_adjoin (F : Type u_1) (E : Type u_2) [] [] [Algebra F E] {α : E} {m : } {n : } (hneq : m n) (heq : Fα ^ m = Fα ^ n) :
theorem Field.isAlgebraic_of_finite_intermediateField (F : Type u_1) (E : Type u_2) [] [] [Algebra F E] [Finite ()] :
@[deprecated Field.FiniteDimensional.of_finite_intermediateField]
theorem Field.finiteDimensional_of_finite_intermediateField (F : Type u_1) (E : Type u_2) [] [] [Algebra F E] [Finite ()] :

Alias of Field.FiniteDimensional.of_finite_intermediateField.

theorem Field.exists_primitive_element_of_finite_intermediateField (F : Type u_1) (E : Type u_2) [] [] [Algebra F E] [Finite ()] (K : ) :
∃ (α : E), Fα = K
theorem Field.FiniteDimensional.of_exists_primitive_element (F : Type u_1) (E : Type u_2) [] [] [Algebra F E] [] (h : ∃ (α : E), Fα = ) :
@[deprecated Field.FiniteDimensional.of_exists_primitive_element]
theorem Field.finiteDimensional_of_exists_primitive_element (F : Type u_1) (E : Type u_2) [] [] [Algebra F E] [] (h : ∃ (α : E), Fα = ) :

Alias of Field.FiniteDimensional.of_exists_primitive_element.

theorem Field.finite_intermediateField_of_exists_primitive_element (F : Type u_1) (E : Type u_2) [] [] [Algebra F E] [] (h : ∃ (α : E), Fα = ) :
theorem Field.exists_primitive_element_iff_finite_intermediateField (F : Type u_1) (E : Type u_2) [] [] [Algebra F E] :
( ∃ (α : E), Fα = ) Finite ()

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.

@[simp]
theorem AlgHom.card (F : Type u_1) (E : Type u_2) [] [] [Algebra F E] [] [] (K : Type u_3) [] [] [Algebra F K] :
@[simp]
theorem AlgHom.card_of_splits (F : Type u_1) (E : Type u_2) [] [] [Algebra F E] [] [] (L : Type u_3) [] [Algebra F L] (hL : ∀ (x : E), Polynomial.Splits () (minpoly F x)) :
theorem Field.primitive_element_iff_minpoly_natDegree_eq (F : Type u_3) {E : Type u_4} [] [] [Algebra F E] [] (α : E) :
Fα = (minpoly F α).natDegree =
theorem Field.primitive_element_iff_minpoly_degree_eq (F : Type u_3) {E : Type u_4} [] [] [Algebra F E] [] (α : E) :
Fα = (minpoly F α).degree =
theorem Field.primitive_element_iff_algHom_eq_of_eval' (F : Type u_3) {E : Type u_4} [] [] [Algebra F E] [] [] (A : Type u_5) [] [Algebra F A] (hA : ∀ (x : E), Polynomial.Splits () (minpoly F x)) (α : E) :
Fα = Function.Injective fun (φ : E →ₐ[F] A) => φ α
theorem Field.primitive_element_iff_algHom_eq_of_eval (F : Type u_3) {E : Type u_4} [] [] [Algebra F E] [] [] (A : Type u_5) [] [Algebra F A] (hA : ∀ (x : E), Polynomial.Splits () (minpoly F x)) (α : E) (φ : E →ₐ[F] A) :
Fα = ∀ (ψ : E →ₐ[F] A), φ α = ψ αφ = ψ