valuation_irreducible_lt_one — Mathlib

English

If ϖ is irreducible in O, then the valuation of its image is strictly less than 1.

Русский

Если ϖ — неприводимый элемент O, то значение v(φ(ϖ)) строго меньше 1.

LaTeX

$$$\operatorname{v}(\mathrm{algebraMap}(O,F)(\varpi)) < 1 \quad \text{для любого неприводимого } \varpi \in O$$$

Lean4

theorem valuation_irreducible_lt_one (hv : Integers v O) {ϖ : O} (h : Irreducible ϖ) : v (algebraMap O F ϖ) < 1 :=
  lt_of_le_of_ne (hv.map_le_one ϖ) (mt hv.isUnit_iff_valuation_eq_one.mpr h.not_isUnit)

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