mathlib documentation

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

@[class]
def normal (F : Type u) (K : Type v) [field F] [field K] [algebra F 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] :
normal F F

theorem normal.is_integral (F : Type u) {K : Type v} [field F] [field K] [algebra F K] [h : normal F K] (x : K) :

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

theorem normal.exists_is_splitting_field (F : Type u) (K : Type v) [field F] [field K] [algebra F K] [normal F K] [finite_dimensional F K] :

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

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

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