finSepDegree_eq_of_isAlgClosed — Mathlib

English

If E/F is algebraic and K/F is algebraically closed, then the separable degree equals the cardinality of F-algebra homomorphisms from E to K.

Русский

Если E/F алгебраично, а K/F алгебраически замкнуто, то сепарабельная степень равна кардинальности множества F-гомоморфизмов E→K.

LaTeX

$$$\operatorname{finSepDegree}(F,E) = |E \to_{F} K|$$$

Lean4

/-- The `Field.finSepDegree F E` is equal to the cardinality of `E →ₐ[F] K` as a natural number,
when `E / F` is algebraic and `K / F` is algebraically closed. -/
@[stacks 09HJ "We use `finSepDegree` to state a more general result."]
theorem finSepDegree_eq_of_isAlgClosed [Algebra.IsAlgebraic F E] [IsAlgClosed K] :
    finSepDegree F E = Nat.card (E →ₐ[F] K) :=
  Nat.card_congr (embEquivOfIsAlgClosed F E K)

Похожие утверждения