finrank — Mathlib

English

For a totally complex K, the degree over Q equals twice the number of complex places: finrank_Q(K) = 2 * nrComplexPlaces(K).

Русский

Для TotallyComplex K степень расширения над Q равна вдвое большему числу комплексных мест: finrank_Q(K) = 2·nrComplexPlaces(K).

LaTeX

$$$\text{IsTotallyComplex}(K) \Rightarrow \operatorname{finrank}_{\mathbb{Q}} K = 2 \cdot nrComplexPlaces(K)$$$

Lean4

protected theorem finrank [h : IsTotallyComplex K] : finrank ℚ K = 2 * nrComplexPlaces K := by
  rw [← card_add_two_mul_card_eq_rank, nrRealPlaces_eq_zero_iff.mpr h, zero_add]

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