v_irreducible_lt_one

Mathlib.RingTheory.Valuation.Integers

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

English

If ϖ is irreducible in the integer-valued setting, then its valuation is less than one.

Русский

Если ϖ — неприводимый в целочисленной обстановке, то его значение меньше единицы.

LaTeX

$${ ϖ : v.integer } Irreducible ϖ → v ϖ < 1$$

Lean4

theorem v_irreducible_lt_one {ϖ : v.integer} (h : Irreducible ϖ) : v ϖ < 1 :=
  (Valuation.integer.integers v).valuation_irreducible_lt_one h

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

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

Разделы

Аффилиация

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