Theorems · Theorem · field theory

Field.finSepDegree_eq_of_adjoin_splits

∀ (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] {S : Set E},
  IntermediateField.adjoin F S = ⊤ →
    (∀ s ∈ S, IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) →
      Field.finSepDegree F E = Nat.card (E →ₐ[F] K)

The Field.finSepDegree F E is equal to the cardinality of E →ₐ[F] K if E = F(S) such that every element s of S is integral (= algebraic) over F and whose minimal polynomial splits in K.

Defined in

Mathlib.FieldTheory.SeparableDegree

Cited by

0 results in Mathlib

Foundations

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

Assumes

FieldFieldAlgebraFieldAlgebra