logEmbedding_component — Mathlib

English

For x ∈ (𝓞 K)ˣ and w ∈ logSpace(K) (represented by w = ⟨place, ≠ w0⟩), the component satisfies (logEmbedding K (Additive.ofMul x)) w = mult w.val × log (w.val x).

Русский

Для x ∈ (𝓞 K)ˣ и w ∈ logSpace(K) выполняется (logEmbedding K (Additive.ofMul x)) w = mult w.val × log (w.val x).

LaTeX

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

Lean4

@[simp]
theorem logEmbedding_component (x : (𝓞 K)ˣ) (w : { w : InfinitePlace K // w ≠ w₀ }) :
    (logEmbedding K (Additive.ofMul x)) w = mult w.val * Real.log (w.val x) :=
  rfl

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