Theorems · Inductive type · field theory

IsNormalClosure

(F : Type u_1) →
  (K : Type u_2) →
    (L : Type u_3) → [inst : Field F] → [inst_1 : Field K] → [inst_2 : Field L] → [Algebra F K] → [Algebra F L] → Prop

L/F is a normal closure of K/F if the minimal polynomial of every element of K over F splits in L, and L is generated by roots of such minimal polynomials over F. (Since the minimal polynomial of a transcendental element is 0, the normal closure of K/F is the same as the normal closure over F of the algebraic closure of F in K.)

Defined in

Mathlib.FieldTheory.Normal.Closure

Cited by

5 results in Mathlib

Foundations

Depth 45 from the axioms · uses propext, Quot.sound

Assumes

FieldFieldFieldAlgebraAlgebra