Theorems · Inductive type · field theory

IsPurelyInseparable

(F : Type u_1) → (E : Type u_2) → [inst : CommRing F] → [inst_1 : Ring E] → [Algebra F E] → Prop

Typeclass for purely inseparable field extensions: an algebraic extension E / F is purely inseparable if and only if the minimal polynomial of every element of E ∖ F is not separable. We define this for general (commutative) rings and only assume F and E are fields if this is needed for a proof.

Defined in

Mathlib.FieldTheory.PurelyInseparable.Basic

Cited by

84 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms

Assumes

CommRingRingAlgebra