logMap_eq_of_normAtPlace_eq — Mathlib

English

If two points have identical norm values at every infinite place, then they share the same logMap value.

Русский

Если у двух точек одинаковы значения норм на всех бесконечных местах, то logMap x = logMap y.

LaTeX

$$$\bigl(\forall w:\text{InfinitePlace }K,\; normAtPlace(w,x)=normAtPlace(w,y)\bigr)\Rightarrow logMap(x)=logMap(y).$$$

Lean4

theorem logMap_eq_of_normAtPlace_eq (h : ∀ w, normAtPlace w x = normAtPlace w y) : logMap x = logMap y :=
  by
  ext
  simp_rw [logMap_apply, h, norm_eq_of_normAtPlace_eq h]

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