# mathlibdocumentation

field_theory.normal

# Normal field extensions

In this file we define normal field extensions and prove that for a finite extension, being normal is the same as being a splitting field (TODO).

## Main Definitions

• normal F K where K is a field extension of F.
@[class]
def normal (F : Type u) (K : Type v) [field F] [field K] [ K] :
Prop

Typeclass for normal field extension: K is a normal extension of F iff the minimal polynomial of every element x in K splits in K, i.e. every conjugate of x is in K.

Equations
• K = ∀ (x : K), ∃ (H : x),
Instances
theorem normal.is_integral (F : Type u) (K : Type v) [field F] [field K] [ K] [h : K] (x : K) :
x

theorem normal.splits (F : Type u) (K : Type v) [field F] [field K] [ K] [h : K] (x : K) :

theorem normal.exists_is_splitting_field (F : Type u) (K : Type v) [field F] [field K] [ K] [ K] [ K] :
∃ (p : ,