English
If E = F(S) with S integral over F and splits in K, then the separable degree of F → E equals the cardinality of the set of F-algebra homomorphisms E → K.
Русский
Если E = F(S) и каждый s ∈ S целочислен над F, а минимальные многочлены распадаются в K, то сепарабельная степень F → E равна кардинальности множества гомоморфизмов E → K, сохраняющих F.
LaTeX
$$$\operatorname{finSepDegree}(F,E) = |E \to_{F} K|$$$
Lean4
/-- 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`. -/
theorem finSepDegree_eq_of_adjoin_splits {S : Set E} (hS : adjoin F S = ⊤)
(hK : ∀ s ∈ S, IsIntegral F s ∧ Splits (algebraMap F K) (minpoly F s)) : finSepDegree F E = Nat.card (E →ₐ[F] K) :=
Nat.card_congr (embEquivOfAdjoinSplits F E K hS hK)
