card_eq_card_isUnramifiedIn — Mathlib

English

The total number of infinite places of K splits as a sum of two parts: unramified over k and its complement, weighted by finrank.

Русский

Общее число бесконечных мест K есть сумма двух частей: безразветвленных над k и их дополнение, взвешенное финразмерностью.

LaTeX

$$If [IsGalois k K] and w : InfinitePlace k with w.IsUnramified k over K, then \\#(InfinitePlace K) = \\#(Unramified over k) \\cdot finrank k K + (complement) \\cdot (finrank k K)/2.$$

Lean4

theorem card_eq_card_isUnramifiedIn [NumberField k] [IsGalois k K] :
    Fintype.card (InfinitePlace K) =
      #{w : InfinitePlace k | w.IsUnramifiedIn K} * finrank k K +
        #({w : InfinitePlace k | w.IsUnramifiedIn K} : Finset _)ᶜ * (finrank k K / 2) :=
  by rw [← card_isUnramified, ← card_isUnramified_compl, Finset.card_add_card_compl]

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