English
If k ⊆ K is Galois, and unramified-at-infinite-places holds, then the total number of infinite places of K equals the product of the number of unramified-in-k places with the degree plus the complementary term weighted by 1/2.
Русский
Если k ⊆ K галлоzово и существует безразветвленность на бесконечных местах, то число бесконечных мест K равно произведению числа бесконечных мест над k на степень расширения плюс дополнительный член, взвешенный наполовину.
LaTeX
$$card(InfinitePlace(K)) = card({w: InfinitePlace k | w.IsUnramifiedIn K}) * finrank k K + #({w: InfinitePlace k | w.IsUnramifiedIn K})ᶜ * (finrank k K / 2).$$
Lean4
theorem card_infinitePlace [NumberField k] [NumberField K] [IsGalois k K] [IsUnramifiedAtInfinitePlaces k K] :
Fintype.card (InfinitePlace K) = Fintype.card (InfinitePlace k) * finrank k K := by
classical
rw [InfinitePlace.card_eq_card_isUnramifiedIn (k := k) (K := K), Finset.filter_true_of_mem, Finset.card_univ,
Finset.card_eq_zero.mpr, zero_mul, add_zero]
· exact Finset.compl_univ
simp only [Finset.mem_univ, forall_true_left]
exact InfinitePlace.isUnramifiedIn K
