norm_irreducible_pos

Mathlib.Topology.Algebra.Valued.LocallyCompact

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

English

If ϖ is irreducible in 𝒪[K], then its norm is positive.

Русский

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

LaTeX

$$$$ \|ϖ\| > 0, \quad ϖ \text{ irreducible} $$

Lean4

theorem norm_irreducible_pos {ϖ : 𝒪[K]} (h : Irreducible ϖ) : 0 < ‖ϖ‖ :=
  Valuation.integer.v_irreducible_pos h

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

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

Разделы

Аффилиация

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