# Documentation

Mathlib.FieldTheory.PrimitiveElement

# 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).

## 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] [] :
α, 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] [] [] :
α, 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, ∀ (α' : E), α' ∀ (β' : E), β' -(α' - α) / (β' - β) ϕ c
theorem Field.primitive_element_inf_aux (F : Type u_1) [] [] {E : Type u_2} [] (α : E) (β : E) [Algebra F E] [] :
γ, Fα, β = Fγ
theorem Field.exists_primitive_element (F : Type u_1) (E : Type u_2) [] [] [Algebra F 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.

Instances For
@[simp]
theorem AlgHom.card (F : Type u_1) (E : Type u_2) (K : Type u_3) [] [] [] [] [Algebra F E] [] [] [Algebra F K] :