Theorems · Theorem · field theory

Field.sepDegree_eq_of_isPurelyInseparable

∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [IsPurelyInseparable F E],
  Field.sepDegree F K = Field.sepDegree E K

If K / E / F is a field extension tower, such that E / F is purely inseparable, then $[K:F]_s = [K:E]_s$. It is a special case of Field.lift_sepDegree_mul_lift_sepDegree_of_isAlgebraic, and is an intermediate result used to prove it.

Defined in

Mathlib.FieldTheory.PurelyInseparable.Tower

Cited by

1 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebraAlgebraIsScalarTowerIsPurelyInseparable