Theorems · Theorem · field theory

IsSeparable.tower_top

∀ {F : Type u_1} (L : Type u_2) [inst : CommRing F] {E : Type u_4} [inst_1 : Field L] [inst_2 : Ring E]
  [inst_3 : Algebra F L] [inst_4 : Algebra F E] [inst_5 : Algebra L E] [IsScalarTower F L E] {x : E},
  IsSeparable F x → IsSeparable L x

If E / L / F is a scalar tower and x : E is separable over F, then it's also separable over L.

Defined in

Mathlib.FieldTheory.Separable

Cited by

11 results in Mathlib

Foundations

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

Assumes

CommRingFieldRingAlgebraAlgebraAlgebraIsScalarTower