norm_pos_of_mem

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

URI: https://scilib.ai/kg/mathlib#NumberField.mixedEmbedding.fundamentalCone.norm_pos_of_mem

English

If x lies in the fundamental cone, then its norm is strictly positive.

Русский

Если x лежит в фундаментальном конусе, то его норма положительна.

LaTeX

$$$x\in\text{fundamentalCone}(K)\Rightarrow 0<\text{mixedEmbedding.norm}(x).$$$

Lean4

theorem norm_pos_of_mem (hx : x ∈ fundamentalCone K) : 0 < mixedEmbedding.norm x :=
  lt_of_le_of_ne (mixedEmbedding.norm_nonneg _) (Ne.symm hx.2)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru