Theorems · Theorem · field theory

IsSeparable.of_algebra_isSeparable_of_isSeparable

∀ (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] [Algebra.IsSeparable F E] {x : K},
  IsSeparable E x → IsSeparable F x

If K / E / F is an extension tower such that E / F is separable, x : K is separable over E, then it's also separable over F.

Defined in

Mathlib.FieldTheory.SeparableDegree

Cited by

3 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebraAlgebraIsScalarTowerAlgebra.IsSeparable