realSpaceToLogSpace_apply — Mathlib

English

For x ≠ 0, the realSpaceToLogSpace of expMap.symm (normAtAllPlaces (mixedEmbedding x)) equals logMap (mixedEmbedding x).

Русский

Для x ≠ 0 выполнено: realSpaceToLogSpace(expMap.symm(normAtAllPlaces(mixedEmbedding x))) = logMap(mixedEmbedding x).

LaTeX

$$$\text{realSpaceToLogSpace}(\expMap^{-1}(\mathrm{normAtAllPlaces}(\mathrm{mixedEmbedding}(x)))) = \logMap(\mathrm{mixedEmbedding}(x))\quad\text{при } x \neq 0$$$

Lean4

theorem realSpaceToLogSpace_apply (x : realSpace K) (w : { w : InfinitePlace K // w ≠ w₀ }) :
    realSpaceToLogSpace x w = x w - w.1.mult * (∑ w', x w') * (Module.finrank ℚ K : ℝ)⁻¹ :=
  rfl

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