sum_mult_eq — Mathlib

English

The sum of the multiplicities over all infinite places equals the ℚ-dimension of K: ∑ w mult(w) = finrank ℚ K.

Русский

Сумма мультипликаторов по всем бесконечным местам равна размерности поля K над ℚ: ∑ mult(w) = finrank ℚ K.

LaTeX

$$$\sum_{w : \mathrm{InfinitePlace}(K)} \operatorname{mult}(w) = \operatorname{finrank}_{\mathbb{Q}} K$$$

Lean4

theorem sum_mult_eq [NumberField K] : ∑ w : InfinitePlace K, mult w = Module.finrank ℚ K := by
  classical
  rw [← Embeddings.card K ℂ, Fintype.card, Finset.card_eq_sum_ones, ←
    Finset.univ.sum_fiberwise (fun φ => InfinitePlace.mk φ)]
  exact Finset.sum_congr rfl (fun _ _ => by rw [Finset.sum_const, smul_eq_mul, mul_one, card_filter_mk_eq])

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