normAtPlace_pos_of_mem — Mathlib

English

For any x in the fundamental cone, the norm at every infinite place is positive.

Русский

Для любой точки x из фундаментального конуса норма на каждом бесконечном месте положительна.

LaTeX

$$$\forall w\in\text{InfinitePlace}(K),\; 0<\text{normAtPlace}(w,x).$$$

Lean4

theorem normAtPlace_pos_of_mem (hx : x ∈ fundamentalCone K) (w : InfinitePlace K) : 0 < normAtPlace w x :=
  lt_of_le_of_ne (normAtPlace_nonneg _ _) (mixedEmbedding.norm_ne_zero_iff.mp (norm_pos_of_mem hx).ne' w).symm

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