toPreorder

Mathlib.RingTheory.Valuation.Basic

URI: https://scilib.ai/kg/mathlib#Valuation.toPreorder

English

A valuation induces a preorder on the ring by x ≤ y iff v(x) ≤ v(y).

Русский

Валуация порождает предпорядок на кольце: x ≤ y тогда и только если v(x) ≤ v(y).

LaTeX

$$$ x \preceq_v y \iff v(x) \le v(y) $$$

Lean4

/-- A valuation gives a preorder on the underlying ring. -/
def toPreorder : Preorder R :=
  Preorder.lift v

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

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

Разделы

Аффилиация

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