Theorems · Inductive type · field theory

Algebra.IsSeparable

(F : Type u_1) → (K : Type u_3) → [inst : CommRing F] → [inst_1 : Ring K] → [Algebra F K] → Prop

Typeclass for separable field extension: K is a separable field extension of F iff the minimal polynomial of every x : K is separable. This implies that K/F is an algebraic extension, because the minimal polynomial of a non-integral element is 0, which is not separable. We define this for general (commutative) rings and only assume F and K are fields if this is needed for a proof.

Defined in

Mathlib.FieldTheory.Separable

Cited by

210 results in Mathlib

Foundations

Depth 6 from the axioms, rests on 21 definitions · uses no axioms

Assumes

CommRingRingAlgebra