logMap_normAtAllPlaces — Mathlib

English

Let K be a number field and x an element in the mixed space associated to K. Then applying the norm at all places and passing to the real-space representation does not change the log map: logMap(mixedSpaceOfRealSpace(normAtAllPlaces x)) = logMap x.

Русский

Пусть K — число планов, x ∈ смешанное пространство(K). Применение норм на всех местах и переход к пространству действительных координат не изменяют логарифмическое отображение: logMap(mixedSpaceOfRealSpace(normAtAllPlaces x)) = logMap x.

LaTeX

$$$\\logMap\\bigl(\\mathrm{mixedSpaceOfRealSpace}(\\operatorname{normAtAllPlaces} \\; x)\\bigr) = \\logMap x$$$

Lean4

theorem logMap_normAtAllPlaces (x : mixedSpace K) : logMap (mixedSpaceOfRealSpace (normAtAllPlaces x)) = logMap x :=
  logMap_eq_of_normAtPlace_eq fun w ↦ by rw [normAtPlace_mixedSpaceOfRealSpace (normAtPlace_nonneg w x)]

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