expMap_sum — Mathlib

English

For a nonzero x in K, the sum over all infinite places of expMap.symm applied to the normAtAllPlaces of x equals the log of the absolute norm of x over ℚ.

Русский

Для ненулевого x сумма по всем бесконечным местам expMap.symm лдя нормAtAllPlaces(x) даёт log(|N_{ℚ}(x)|).

LaTeX

$$$\\sum_{w} \\expMap.symm(\\operatorname{normAtAllPlaces}(\\mathrm{mixedEmbedding}(K, x))) w = \\log(|\\mathrm{Algebra.norm}_{\\mathbb{Q}}(x)|)$$$

Lean4

theorem expMap_sum {ι : Type*} (s : Finset ι) (f : ι → realSpace K) : expMap (∑ i ∈ s, f i) = ∏ i ∈ s, expMap (f i) :=
  by
  ext
  simp [← Real.exp_sum, ← mul_sum]

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