Structures · Algebra

Algebra.IsSeparable

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

Shape

2 explicit arguments · adds isSeparable'