card_eq_nrRealPlaces_add_nrComplexPlaces

English

The total number of infinite places of K equals the sum of real and complex places: card(InfinitePlace K) = nrRealPlaces K + nrComplexPlaces K.

Русский

Общее число бесконечных мест поля K равно сумме числа действительных мест и числа комплексных мест.

LaTeX

$$$|\mathrm{InfinitePlace}(K)| = nrRealPlaces(K) + nrComplexPlaces(K).$$$

Lean4

theorem card_eq_nrRealPlaces_add_nrComplexPlaces :
    Fintype.card (InfinitePlace K) = nrRealPlaces K + nrComplexPlaces K := by
  classical
  convert Fintype.card_subtype_or_disjoint (IsReal (K := K)) (IsComplex (K := K)) (disjoint_isReal_isComplex K) using 1
  exact (Fintype.card_of_subtype _ (fun w ↦ ⟨fun _ ↦ isReal_or_isComplex w, fun _ ↦ by simp⟩)).symm

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