v_irreducible_pos

Mathlib.RingTheory.Valuation.Integers

URI: https://scilib.ai/kg/mathlib#Valuation.integer.v_irreducible_pos

English

For irreducible ϖ in O, v(φ(ϖ)) > 0.

Русский

Для неприводимого ϖ в O: v(φ(ϖ)) > 0.

LaTeX

$$0 < v(\mathrm{algebraMap}(O,F)(\varpi))$$

Lean4

theorem v_irreducible_pos {ϖ : v.integer} (h : Irreducible ϖ) : 0 < v ϖ :=
  (Valuation.integer.integers v).valuation_irreducible_pos h

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

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

Разделы

Аффилиация

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