logMap_apply_of_norm_one — Mathlib

English

There is a MulAction of (𝓞 K)ˣ on the mixedSpace, and it respects multiplication in the base ring.

Русский

Существует MulAction (𝓞 K)ˣ на смешанном пространстве, и он сохраняет умножение в базовом кольце.

LaTeX

$$MulAction ((\mathcal{O}_K)^{\times}) (mixedSpace K) with \cdot and * compatibility$$

Lean4

theorem logMap_apply_of_norm_one (hx : mixedEmbedding.norm x = 1) (w : { w : InfinitePlace K // w ≠ w₀ }) :
    logMap x w = mult w.val * Real.log (normAtPlace w x) := by rw [logMap_apply, hx, Real.log_one, zero_mul, sub_zero]

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