Theorems · Theorem · field theory

isPurelyInseparable_iff_natSepDegree_eq_one

∀ (F : Type u) {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  IsPurelyInseparable F E ↔ ∀ (x : E), (minpoly F x).natSepDegree = 1

A field extension E / F is purely inseparable if and only if for every element x of E, its minimal polynomial has separable degree one.

Defined in

Mathlib.FieldTheory.PurelyInseparable.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra