Theorems · Inductive type · field theory

Normal

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

Typeclass for normal field extensions: an algebraic extension of fields K/F is normal if the minimal polynomial of every element x in K splits in K, i.e. every F-conjugate of x is in K.

Defined in

Mathlib.FieldTheory.Normal.Defs

Cited by

92 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra