valuation_irreducible_pos — Mathlib

English

Irreducible elements map to strictly positive valuation

Русский

Неприводимые элементы отображаются с положительным значением оценивания.

LaTeX

$$$0 < v(\mathrm{algebraMap}(O,F)(\varpi)) \text{ для неразложимого } \varpi$$$

Lean4

theorem valuation_irreducible_pos (hv : Integers v O) {ϖ : O} (h : Irreducible ϖ) : 0 < v (algebraMap O F ϖ) :=
  hv.valuation_pos_iff_ne_zero.mpr h.ne_zero

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