card_add_two_mul_card_eq_rank — Mathlib

English

The real places plus twice the complex places equals the total Q-rank: nrRealPlaces K + 2 nrComplexPlaces K = finrankℚ K.

Русский

Число действительных мест плюс дважды число комплексных мест равны порядку поля над \mathbb{Q}.

LaTeX

$$nrRealPlaces(K) + 2 \cdot nrComplexPlaces(K) = \operatorname{finrank}_{\mathbb{Q}} K.$$

Lean4

theorem card_add_two_mul_card_eq_rank : nrRealPlaces K + 2 * nrComplexPlaces K = finrank ℚ K := by
  classical
  rw [← card_real_embeddings, ← card_complex_embeddings, Fintype.card_subtype_compl, ← Embeddings.card K ℂ,
    Nat.add_sub_of_le]
  exact Fintype.card_subtype_le _

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