sum_logEmbedding_component — Mathlib

English

The sum over all w of logEmbedding equals minus mult w0 times log at w0.

Русский

Сумма по всем w логарифмических вложений равна минус mult w0 умноженное на log на w0.

LaTeX

$$$\sum_w \logEmbedding K (Additive.ofMul x)\, w = -\mathrm{mult}(w_0) \cdot \log(w_0(x))$$$

Lean4

theorem sum_logEmbedding_component (x : (𝓞 K)ˣ) :
    ∑ w, logEmbedding K (Additive.ofMul x) w = -mult (w₀ : InfinitePlace K) * Real.log (w₀ (x : K)) :=
  by
  have h := sum_mult_mul_log x
  rw [Fintype.sum_eq_add_sum_subtype_ne _ w₀, add_comm, add_eq_zero_iff_eq_neg, ← neg_mul] at h
  simpa [logEmbedding_component] using h

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