# 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
Instances
@[instance]
def normal_self (F : Type u) [field F] :
F

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) :
(minpoly F x)

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

theorem normal.tower_top_of_normal (F : Type u) (K : Type v) [field F] [field K] [ K] (E : Type u_1) [field E] [ E] [ E] [ E] [h : E] :
E

theorem normal.of_alg_equiv {F : Type u} [field F] {E : Type u_1} [field E] [ E] {E' : Type u_2} [field E'] [ E'] [h : E] (f : E ≃ₐ[F] E') :
E'

theorem alg_equiv.transfer_normal {F : Type u} [field F] {E : Type u_1} [field E] [ E] {E' : Type u_2} [field E'] [ E'] (f : E ≃ₐ[F] E') :
E E'