cardinal_eq_of_isSeparable — Mathlib

English

If E is algebraic over F, then the number of F-embeddings of E into an algebraic closure equals 2 raised to the separable degree of E over F.

Русский

Если E над F алгебраически, число вложений E в алг Closure равно 2^{sepDegree_F E}.

LaTeX

$$$\\#(\\mathrm{Field Emb } F E) = 2^{\\mathrm{sepDegree} F E}$$$

Lean4

theorem cardinal_eq_of_isSeparable [Algebra.IsSeparable F E] :
    #(Field.Emb F E) = (fun c ↦ if ℵ₀ ≤ c then 2 ^ c else c) (Module.rank F E) :=
  by
  dsimp only; split_ifs with h
  · exact cardinal_eq_two_pow_rank h
  rw [not_le, ← IsNoetherian.iff_rank_lt_aleph0] at h
  rw [← Module.finrank_eq_rank, ← toNat_eq_iff Module.finrank_pos.ne', ← Nat.card, ← finSepDegree,
    finSepDegree_eq_finrank_of_isSeparable]

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