Theorems · Theorem · field theory

IntermediateField.finSepDegree_adjoin_simple_eq_finrank_iff

∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
  IsAlgebraic F α → (Field.finSepDegree F ↥F⟮α⟯ = Module.finrank F ↥F⟮α⟯ ↔ IsSeparable F α)

If α is algebraic over F, then the separable degree of F⟮α⟯ / F is equal to the degree of F⟮α⟯ / F if and only if α is a separable element.

Defined in

Mathlib.FieldTheory.SeparableDegree

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebra