sum_mult_mul_log — Mathlib

English

For a number field K and a unit x ∈ 𝓞K, the total logarithmic contribution across all places vanishes: the sum of w.mult · log w x over all infinite places equals zero.

Русский

Для числа поля K и единицы x ∈ 𝓞K сумма логарифмов по всем местам даёт ноль: сумма w.mult · log w x по всем бесконечным местам равна нулю.

LaTeX

$$∑_{w ∈ InfinitePlace(K)} w.mult · log w x = 0$$

Lean4

theorem sum_mult_mul_log [NumberField K] (x : (𝓞 K)ˣ) : ∑ w : InfinitePlace K, w.mult * Real.log (w x) = 0 := by
  simpa [Units.norm, Real.log_prod, Real.log_pow] using congr_arg Real.log (prod_eq_abs_norm (x : K))

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