finrank — Mathlib

English

For a totally real field K, the degree of K over Q equals the number of real places: finrank_Q(K) = nrRealPlaces(K).

Русский

Для полностью вещественного поля K степень расширения K/Q равна числу вещественных мест: finrank_Q(K) = nrRealPlaces(K).

LaTeX

$$$\text{IsTotallyReal}(K) \implies \operatorname{finrank}_{\mathbb{Q}} K = nrRealPlaces(K)$$$

Lean4

protected theorem finrank [h : IsTotallyReal K] : finrank ℚ K = nrRealPlaces K := by
  rw [← card_add_two_mul_card_eq_rank, nrComplexPlaces_eq_zero_iff.mpr h, mul_zero, add_zero]

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