Theorems · Theorem · field theory

IntermediateField.isSeparable_adjoin_simple_iff_isSeparable

∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {x : E},
  Algebra.IsSeparable F ↥F⟮x⟯ ↔ IsSeparable F x

F⟮x⟯ / F is a separable extension if and only if x is a separable element. As a consequence, any rational function of x is also a separable element.

Defined in

Mathlib.FieldTheory.SeparableDegree

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra