# mathlibdocumentation

field_theory.primitive_element

# 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 is_primitive_element 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_fintype_top (F : Type u_1) [field F] (E : Type u_2) [field E] [ E] [fintype E] :
∃ (α : E), Fα =

Primitive element theorem assuming E is finite.

theorem field.exists_primitive_element_of_fintype_bot (F : Type u_1) [field F] (E : Type u_2) [field E] [ E] [fintype 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} [field F] [infinite F] {E : Type u_2} [field E] (ϕ : F →+* E) (α β : E) (f g : polynomial F) :
∃ (c : F), ∀ (α' : E), α' f).roots∀ (β' : E), β' g).roots-(α' - α) / (β' - β) ϕ c
theorem field.primitive_element_inf_aux (F : Type u_1) [field F] [infinite F] {E : Type u_2} [field E] (α β : E) [ E] [ E] :
∃ (γ : E), Fα, β = Fγ
theorem field.exists_primitive_element (F : Type u_1) (E : Type u_2) [field F] [field E] [ E] [ E] [ 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.power_basis_of_finite_of_separable (F : Type u_1) (E : Type u_2) [field F] [field E] [ E] [ E] [ E] :
E

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

See also exists_primitive_element.

Equations
noncomputable def field.fintype.subtype_prod {E : Type u_1} {X : set E} (hX : X.finite) {L : Type u_2} (F : E → ) :
fintype (Π (x : X), {l // l F x})

A technical finiteness result.

Equations
def field.roots_of_min_poly_pi_type (F : Type u_1) (E : Type u_2) [field F] [field E] [ E] [ E] (K : Type u_3) [field K] [ K] (φ : E →ₐ[F] K) (x : ) :
{l // l (polynomial.map K) (minpoly F x.val)).roots}

Function from Hom_K(E,L) to pi type Π (x : basis), roots of min poly of x

Equations
theorem field.aux_inj_roots_of_min_poly (F : Type u_1) (E : Type u_2) [field F] [field E] [ E] [ E] (K : Type u_3) [field K] [ K] :
@[protected, instance]
noncomputable def field.alg_hom.fintype (F : Type u_1) (E : Type u_2) [field F] [field E] [ E] [ E] (K : Type u_3) [field K] [ K] :

Given field extensions E/F and K/F, with E/F finite, there are finitely many F-algebra homomorphisms E →ₐ[K] K.

Equations
@[simp]
theorem alg_hom.card (F : Type u_1) (E : Type u_2) (K : Type u_3) [field F] [field E] [field K] [ E] [ E] [ E] [ K] :