norm_le_one

Mathlib.Topology.Algebra.Valued.LocallyCompact

URI: https://scilib.ai/kg/mathlib#Valued.integer.norm_le_one

English

If x lies in the valuation ring 𝒪[K], then its norm is at most 1.

Русский

Если x лежит в кольце оценки 𝒪[K], то его норма не превосходит единицы.

LaTeX

$$$$ x \in 𝒪[K] \implies \|x\| \le 1 $$$$

Lean4

theorem norm_le_one (x : 𝒪[K]) : ‖x‖ ≤ 1 :=
  mem_iff.mp x.prop

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

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

Разделы

Аффилиация

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