finrank — Mathlib

English

For a number field K, the real dimension of the mixed space equals the degree of K over Q: finrank_R(mixedSpace K) = finrank_Q K.

Русский

Для числа поля K вещественный размер пространства слияния равен степени расширения [K:Q].

LaTeX

$$$\operatorname{finrank}_{\mathbb{R}}(\mathrm{mixedSpace}(K)) = \operatorname{finrank}_{\mathbb{Q}} K.$$$

Lean4

protected theorem finrank [NumberField K] : finrank ℝ (mixedSpace K) = finrank ℚ K := by
  classical
    rw [finrank_prod, finrank_pi, finrank_pi_fintype, Complex.finrank_real_complex, sum_const, card_univ, ←
    nrRealPlaces, ← nrComplexPlaces, ← card_real_embeddings, Algebra.id.smul_eq_mul, mul_comm, ←
    card_complex_embeddings, ← NumberField.Embeddings.card K ℂ, Fintype.card_subtype_compl,
    Nat.add_sub_of_le (Fintype.card_subtype_le _)]

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