norm_nonneg

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic

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

English

The global norm is always nonnegative for any x.

Русский

Глобальная норма всегда неотрицательна для любого x.

LaTeX

$$$ 0 \le \|x\| $$$

Lean4

protected theorem norm_nonneg (x : mixedSpace K) : 0 ≤ mixedEmbedding.norm x :=
  univ.prod_nonneg fun _ _ ↦ pow_nonneg (normAtPlace_nonneg _ _) _

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

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

Разделы

Аффилиация

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