Theorems · Definition · field theory

IsSeparable

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

An element x of an algebra K over a commutative ring F is said to be separable, if its minimal polynomial over K is separable. Note that the minimal polynomial of any element not integral over F is defined to be 0, which is not a separable polynomial.

Defined in

Mathlib.FieldTheory.Separable

Cited by

68 results in Mathlib

Foundations

Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingRingAlgebra