norm_irreducible_lt_one

Mathlib.Topology.Algebra.Valued.LocallyCompact

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

English

If ϖ is irreducible in 𝒪[K], then its norm is less than 1.

Русский

Если ϖ неприводим в 𝒪[K], то его норма меньше 1.

LaTeX

$$$$ \|\varpi\| < 1, \quad \varpi \text{ irreducible in } 𝒪[K] $$$$

Lean4

theorem norm_irreducible_lt_one {ϖ : 𝒪[K]} (h : Irreducible ϖ) : ‖ϖ‖ < 1 :=
  Valuation.integer.v_irreducible_lt_one h

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

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

Разделы

Аффилиация

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