normAtAllPlaces_apply — Mathlib

English

Let x be an element of the mixed space and w be an infinite place. Then the value of the norm at all places evaluated at x and w equals the place-wise norm of x at w.

Русский

Пусть x ∈ смещённое пространство и w — бесконечное место. Тогда значение нормы на всех местах, применённое к x и w, равно норме на месте w, применённой к x.

LaTeX

$$$\forall x, w,\quad \operatorname{normAtAllPlaces}(x, w) = \operatorname{normAtPlace}(w, x)$$$

Lean4

@[simp]
theorem normAtAllPlaces_apply (x : mixedSpace K) (w : InfinitePlace K) : normAtAllPlaces x w = normAtPlace w x :=
  rfl

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