cardinal_eq — Mathlib

English

If E is separable over F, then the cardinality of Field.Emb F E equals 2^sepDegree F E.

Русский

Если поле E сепарабельно над F, то число вложений равно 2^{sepDegree F E}.

LaTeX

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

Lean4

theorem cardinal_eq [Algebra.IsAlgebraic F E] :
    #(Field.Emb F E) = (fun c ↦ if ℵ₀ ≤ c then 2 ^ c else c) (sepDegree F E) := by
  rw [← cardinal_separableClosure, cardinal_eq_of_isSeparable]; rfl

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