norm_nonneg

Mathlib.Topology.Algebra.Valued.NormedValued

URI: https://scilib.ai/kg/mathlib#Valued.norm_nonneg

English

If the valuation ring is compact, then it is a discrete valuation ring (DVR).

Русский

Если кольцо оценки компактно, то оно дискретное кольцо оценки.

LaTeX

$$$$ 𝒪_K \text{ is a DVR}. $$$$

Lean4

theorem norm_nonneg (x : L) : 0 ≤ norm x := by simp only [norm, NNReal.zero_le_coe]

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

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

Разделы

Аффилиация

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