Valuative Relations

In this file we introduce a class called ValuativeRel R for a ring R. This bundles a relation vle : R → R → Prop on R which mimics a preorder on R arising from a valuation. We introduce the notation x ≤ᵥ y for this relation.

Recall that the equivalence class of a valuation is completely characterized by such a preorder. Thus, we can think of ValuativeRel R as a way of saying that R is endowed with an equivalence class of valuations.

Main Definitions

• ValuativeRel R endows a commutative ring R with a relation arising from a valuation. This is equivalent to fixing an equivalence class of valuations on R. Use the notation x ≤ᵥ y for this relation.
• ValuativeRel.valuation R is the "canonical" valuation associated to ValuativeRel R, taking values in ValuativeRel.ValueGroupWithZero R.
• Given a valuation v on R and an instance [ValuativeRel R], writing [v.Compatible] ensures that the relation x ≤ᵥ y is equivalent to v x ≤ v y. Note that it is possible to have [v.Compatible] and [w.Compatible] for two different valuations on R.
• Given [ValuativeRel A], [ValuativeRel B] and [Algebra A B], the class [ValuativeExtension A B] ensures that the algebra map A → B is compatible with the valuations on A and B. For example, this can be used to talk about extensions of valued fields.

Remark

The last two axioms in ValuativeRel, namely vle_mul_cancel and not_vle_one_zero, are used to ensure that we have a well-behaved valuation taking values in a value group (with zero). In principle, it should be possible to drop these two axioms and obtain a value monoid, however, such a value monoid would not necessarily embed into an ordered abelian group with zero. Similarly, without these axioms, the support of the valuation need not be a prime ideal. We have thus opted to include these two axioms and obtain a ValueGroupWithZero associated to a ValuativeRel in order to best align with the literature about valuations on commutative rings.

Future work could refactor ValuativeRel by dropping the vle_mul_cancel and not_vle_one_zero axioms, opting to make these mixins instead.

Projects

The ValuativeRel class should eventually replace the existing Valued typeclass. Once such a refactor happens, ValuativeRel could be renamed to Valued.

TODO

Split this file. For instance, the universal properties of ValueGroupWithZero and definition of IsRankLeOne could be separated out.

class ValuativeRel (R : Type u_1) [CommRing R] : Type u_1

The class [ValuativeRel R] class introduces an operator x ≤ᵥ y : Prop for x y : R which is the natural relation arising from (the equivalence class of) a valuation on R. More precisely, if v is a valuation on R then the associated relation is x ≤ᵥ y ↔ v x ≤ v y. Use this class to talk about the case where R is equipped with an equivalence class of valuations.

• vle : R → R → Prop

  The valuation less-equal operator arising from ValuativeRel.

• vle_total (x y : R) : x ≤ᵥ y ∨ y ≤ᵥ x
• vle_trans {z y x : R} : x ≤ᵥ y → y ≤ᵥ z → x ≤ᵥ z
• vle_add {x y z : R} : x ≤ᵥ z → y ≤ᵥ z → x + y ≤ᵥ z
• mul_vle_mul_left {x y : R} (h : x ≤ᵥ y) (z : R) : x * z ≤ᵥ y * z
• vle_mul_cancel {x y z : R} : ¬z ≤ᵥ 0 → x * z ≤ᵥ y * z → x ≤ᵥ y
• not_vle_one_zero : ¬1 ≤ᵥ 0

theorem ValuativeRel.ext {R : Type u_1} {inst✝ : CommRing R} {x y : ValuativeRel R} (vle : vle = vle) : x = y

theorem ValuativeRel.ext_iff {R : Type u_1} {inst✝ : CommRing R} {x y : ValuativeRel R} : x = y ↔ vle = vle

def «term_≤ᵥ_» : Lean.TrailingParserDescr

The valuation less-equal operator arising from ValuativeRel.

Equations

• «term_≤ᵥ_» = Lean.ParserDescr.trailingNode `«term_≤ᵥ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≤ᵥ ") (Lean.ParserDescr.cat `term 51))

class Valuation.Compatible {R : Type u_1} {Γ : Type u_2} [CommRing R] [LinearOrderedCommMonoidWithZero Γ] (v : Valuation R Γ) [ValuativeRel R] : Prop

We say that a valuation v is Compatible if the relation x ≤ᵥ y is equivalent to v x ≤ v y.

• vle_iff_le (x y : R) : x ≤ᵥ y ↔ v x ≤ v y

class ValuativePreorder (R : Type u_1) [CommRing R] [ValuativeRel R] [Preorder R] : Prop

A preorder on a ring is said to be "valuative" if it agrees with the valuative relation.

• vle_iff_le (x y : R) : x ≤ᵥ y ↔ x ≤ y

@[deprecated ValuativeRel.vle (since := "2025-12-20")]

def ValuativeRel.Rel {R : Type u_1} {inst✝ : CommRing R} [self : ValuativeRel R] : R → R → Prop

Alias of ValuativeRel.vle.

---

The valuation less-equal operator arising from ValuativeRel.

Equations

• @ValuativeRel.Rel = @ValuativeRel.vle

@[deprecated ValuativeRel.vle_total (since := "2025-12-20")]

theorem ValuativeRel.rel_total {R : Type u_1} {inst✝ : CommRing R} [self : ValuativeRel R] (x y : R) : x ≤ᵥ y ∨ y ≤ᵥ x

Alias of ValuativeRel.vle_total.

@[deprecated ValuativeRel.vle_trans (since := "2025-12-20")]

theorem ValuativeRel.rel_trans {R : Type u_1} {inst✝ : CommRing R} [self : ValuativeRel R] {z y x : R} : x ≤ᵥ y → y ≤ᵥ z → x ≤ᵥ z

Alias of ValuativeRel.vle_trans.

@[deprecated ValuativeRel.vle_add (since := "2025-12-20")]

theorem ValuativeRel.rel_add {R : Type u_1} {inst✝ : CommRing R} [self : ValuativeRel R] {x y z : R} : x ≤ᵥ z → y ≤ᵥ z → x + y ≤ᵥ z

Alias of ValuativeRel.vle_add.

@[deprecated ValuativeRel.mul_vle_mul_left (since := "2025-12-20")]

theorem ValuativeRel.rel_mul_right {R : Type u_1} {inst✝ : CommRing R} [self : ValuativeRel R] {x y : R} (h : x ≤ᵥ y) (z : R) : x * z ≤ᵥ y * z

Alias of ValuativeRel.mul_vle_mul_left.

@[deprecated ValuativeRel.vle_mul_cancel (since := "2025-12-20")]

theorem ValuativeRel.rel_mul_cancel {R : Type u_1} {inst✝ : CommRing R} [self : ValuativeRel R] {x y z : R} : ¬z ≤ᵥ 0 → x * z ≤ᵥ y * z → x ≤ᵥ y

Alias of ValuativeRel.vle_mul_cancel.

@[deprecated ValuativeRel.not_vle_one_zero (since := "2025-12-20")]

theorem ValuativeRel.not_rel_one_zero {R : Type u_1} {inst✝ : CommRing R} [self : ValuativeRel R] : ¬1 ≤ᵥ 0

Alias of ValuativeRel.not_vle_one_zero.

def ValuativeRel.vlt {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) : Prop

The valuation less-than relation, defined as x <ᵥ y ↔ ¬ y ≤ᵥ x.

Equations

• (x <ᵥ y) = ¬y ≤ᵥ x

@[deprecated ValuativeRel.vlt (since := "2025-12-20")]

def ValuativeRel.SRel {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) : Prop

Alias of ValuativeRel.vlt.

---

The valuation less-than relation, defined as x <ᵥ y ↔ ¬ y ≤ᵥ x.

Equations

• @ValuativeRel.SRel = @ValuativeRel.vlt

def ValuativeRel.«term_<ᵥ_» : Lean.TrailingParserDescr

The valuation less-than relation, defined as x <ᵥ y ↔ ¬ y ≤ᵥ x.

Equations

• ValuativeRel.«term_<ᵥ_» = Lean.ParserDescr.trailingNode `ValuativeRel.«term_<ᵥ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " <ᵥ ") (Lean.ParserDescr.cat `term 51))

def ValuativeRel.veq {R : Type u_1} [CommRing R] [ValuativeRel R] : R → R → Prop

The valuation equals relation, defined as x =ᵥ y ↔ x ≤ᵥ y ∧ y ≤ᵥ x.

Equations

• ValuativeRel.veq = AntisymmRel fun (x1 x2 : R) => x1 ≤ᵥ x2

def ValuativeRel.«term_=ᵥ_» : Lean.TrailingParserDescr

The valuation equals relation, defined as x =ᵥ y ↔ x ≤ᵥ y ∧ y ≤ᵥ x.

Equations

• ValuativeRel.«term_=ᵥ_» = Lean.ParserDescr.trailingNode `ValuativeRel.«term_=ᵥ_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " =ᵥ ") (Lean.ParserDescr.cat `term 51))

@[simp]

theorem ValuativeRel.not_vle {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} : ¬x ≤ᵥ y ↔ y <ᵥ x

@[simp]

theorem ValuativeRel.not_vlt {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} : ¬x <ᵥ y ↔ y ≤ᵥ x

theorem ValuativeRel.veq_def {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} : x =ᵥ y ↔ x ≤ᵥ y ∧ y ≤ᵥ x

@[deprecated ValuativeRel.not_vle (since := "2025-12-20")]

theorem ValuativeRel.srel_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} : x <ᵥ y ↔ ¬y ≤ᵥ x

@[deprecated ValuativeRel.not_vlt (since := "2025-12-20")]

theorem ValuativeRel.not_srel_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} : ¬x <ᵥ y ↔ y ≤ᵥ x

Alias of ValuativeRel.not_vlt.

theorem ValuativeRel.vle.not_vlt {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} : y ≤ᵥ x → ¬x <ᵥ y

Alias of the reverse direction of ValuativeRel.not_vlt.

theorem ValuativeRel.vlt.not_vle {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} : y <ᵥ x → ¬x ≤ᵥ y

Alias of the reverse direction of ValuativeRel.not_vle.

theorem ValuativeRel.veq_comm {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} : x =ᵥ y ↔ y =ᵥ x

theorem ValuativeRel.veq.symm {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} : x =ᵥ y → y =ᵥ x

Alias of the forward direction of ValuativeRel.veq_comm.

instance ValuativeRel.instSymmVeq {R : Type u_1} [CommRing R] [ValuativeRel R] : Std.Symm fun (x1 x2 : R) => x1 =ᵥ x2

theorem ValuativeRel.vle_of_veq {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (h : x =ᵥ y) : x ≤ᵥ y

theorem ValuativeRel.vge_of_veq {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (h : x =ᵥ y) : y ≤ᵥ x

theorem ValuativeRel.veq.vle {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (h : x =ᵥ y) : x ≤ᵥ y

Alias of ValuativeRel.vle_of_veq.

theorem ValuativeRel.veq.vge {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (h : x =ᵥ y) : y ≤ᵥ x

Alias of ValuativeRel.vge_of_veq.

theorem ValuativeRel.not_vlt_of_veq {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (h : x =ᵥ y) : ¬x <ᵥ y

theorem ValuativeRel.not_vgt_of_veq {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (h : x =ᵥ y) : ¬y <ᵥ x

theorem ValuativeRel.veq.not_vlt {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (h : x =ᵥ y) : ¬x <ᵥ y

Alias of ValuativeRel.not_vlt_of_veq.

theorem ValuativeRel.veq.not_vgt {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (h : x =ᵥ y) : ¬y <ᵥ x

Alias of ValuativeRel.not_vgt_of_veq.

@[simp]

theorem ValuativeRel.vle_refl {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : x ≤ᵥ x

theorem ValuativeRel.vle_rfl {R : Type u_1} [CommRing R] [ValuativeRel R] {x : R} : x ≤ᵥ x

@[deprecated ValuativeRel.vle_refl (since := "2025-12-20")]

theorem ValuativeRel.rel_refl {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : x ≤ᵥ x

Alias of ValuativeRel.vle_refl.

@[deprecated ValuativeRel.vle_rfl (since := "2025-12-20")]

theorem ValuativeRel.rel_rfl {R : Type u_1} [CommRing R] [ValuativeRel R] {x : R} : x ≤ᵥ x

Alias of ValuativeRel.vle_rfl.

theorem ValuativeRel.vle.refl {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : x ≤ᵥ x

Alias of ValuativeRel.vle_refl.

theorem ValuativeRel.vle.rfl {R : Type u_1} [CommRing R] [ValuativeRel R] {x : R} : x ≤ᵥ x

Alias of ValuativeRel.vle_rfl.

instance ValuativeRel.instReflVle {R : Type u_1} [CommRing R] [ValuativeRel R] : Std.Refl fun (x1 x2 : R) => x1 ≤ᵥ x2

@[deprecated ValuativeRel.vle.refl (since := "2025-12-20")]

theorem ValuativeRel.Rel.refl {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : x ≤ᵥ x

Alias of ValuativeRel.vle_refl.

---

Alias of ValuativeRel.vle_refl.

@[deprecated ValuativeRel.vle.rfl (since := "2025-12-20")]

theorem ValuativeRel.Rel.rfl {R : Type u_1} [CommRing R] [ValuativeRel R] {x : R} : x ≤ᵥ x

Alias of ValuativeRel.vle_rfl.

---

Alias of ValuativeRel.vle_rfl.

@[simp]

theorem ValuativeRel.veq_refl {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : x =ᵥ x

theorem ValuativeRel.veq_rfl {R : Type u_1} [CommRing R] [ValuativeRel R] {x : R} : x =ᵥ x

theorem ValuativeRel.veq.refl {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : x =ᵥ x

Alias of ValuativeRel.veq_refl.

theorem ValuativeRel.veq.rfl {R : Type u_1} [CommRing R] [ValuativeRel R] {x : R} : x =ᵥ x

Alias of ValuativeRel.veq_rfl.

instance ValuativeRel.instReflVeq {R : Type u_1} [CommRing R] [ValuativeRel R] : Std.Refl fun (x1 x2 : R) => x1 =ᵥ x2

@[simp]

theorem ValuativeRel.zero_vle {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : 0 ≤ᵥ x

@[deprecated ValuativeRel.zero_vle (since := "2025-12-20")]

theorem ValuativeRel.zero_rel {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : 0 ≤ᵥ x

Alias of ValuativeRel.zero_vle.

@[simp]

theorem ValuativeRel.not_vlt_zero {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : ¬x <ᵥ 0

theorem ValuativeRel.vlt.ne_zero {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (h : x <ᵥ y) : y ≠ 0

@[simp]

theorem ValuativeRel.zero_vlt_one {R : Type u_1} [CommRing R] [ValuativeRel R] : 0 <ᵥ 1

@[deprecated ValuativeRel.zero_vlt_one (since := "2025-12-20")]

theorem ValuativeRel.zero_srel_one {R : Type u_1} [CommRing R] [ValuativeRel R] : 0 <ᵥ 1

Alias of ValuativeRel.zero_vlt_one.

@[deprecated ValuativeRel.mul_vle_mul_left (since := "2026-01-06")]

theorem ValuativeRel.vle_mul_right {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (z : R) (h : x ≤ᵥ y) : x * z ≤ᵥ y * z

theorem ValuativeRel.mul_vle_mul_right {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (h : x ≤ᵥ y) (z : R) : z * x ≤ᵥ z * y

@[deprecated ValuativeRel.mul_vle_mul_right (since := "2025-12-20")]

theorem ValuativeRel.rel_mul_left {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (h : x ≤ᵥ y) (z : R) : z * x ≤ᵥ z * y

Alias of ValuativeRel.mul_vle_mul_right.

@[implicit_reducible]

instance ValuativeRel.instTransVle {R : Type u_1} [CommRing R] [ValuativeRel R] : Trans vle vle vle

Equations

• ValuativeRel.instTransVle = { trans := ⋯ }

theorem ValuativeRel.vle.trans {R : Type u_1} {inst✝ : CommRing R} [self : ValuativeRel R] {z y x : R} : x ≤ᵥ y → y ≤ᵥ z → x ≤ᵥ z

Alias of ValuativeRel.vle_trans.

@[deprecated ValuativeRel.vle.trans (since := "2025-12-20")]

theorem ValuativeRel.Rel.trans {R : Type u_1} {inst✝ : CommRing R} [self : ValuativeRel R] {z y x : R} : x ≤ᵥ y → y ≤ᵥ z → x ≤ᵥ z

Alias of ValuativeRel.vle_trans.

---

Alias of ValuativeRel.vle_trans.

theorem ValuativeRel.vle_trans' {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (h1 : y ≤ᵥ z) (h2 : x ≤ᵥ y) : x ≤ᵥ z

@[deprecated ValuativeRel.vle_trans' (since := "2025-12-20")]

theorem ValuativeRel.rel_trans' {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (h1 : y ≤ᵥ z) (h2 : x ≤ᵥ y) : x ≤ᵥ z

Alias of ValuativeRel.vle_trans'.

theorem ValuativeRel.vle.trans' {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (h1 : y ≤ᵥ z) (h2 : x ≤ᵥ y) : x ≤ᵥ z

Alias of ValuativeRel.vle_trans'.

@[deprecated ValuativeRel.vle.trans' (since := "2025-12-20")]

theorem ValuativeRel.Rel.trans' {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (h1 : y ≤ᵥ z) (h2 : x ≤ᵥ y) : x ≤ᵥ z

Alias of ValuativeRel.vle_trans'.

---

Alias of ValuativeRel.vle_trans'.

theorem ValuativeRel.veq_trans {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (h1 : x =ᵥ y) (h2 : y =ᵥ z) : x =ᵥ z

@[implicit_reducible]

instance ValuativeRel.instTransVeq {R : Type u_1} [CommRing R] [ValuativeRel R] : Trans veq veq veq

Equations

• ValuativeRel.instTransVeq = { trans := ⋯ }

theorem ValuativeRel.mul_vle_mul {R : Type u_1} [CommRing R] [ValuativeRel R] {x x' y y' : R} (h1 : x ≤ᵥ y) (h2 : x' ≤ᵥ y') : x * x' ≤ᵥ y * y'

@[deprecated ValuativeRel.mul_vle_mul (since := "2025-12-20")]

theorem ValuativeRel.mul_rel_mul {R : Type u_1} [CommRing R] [ValuativeRel R] {x x' y y' : R} (h1 : x ≤ᵥ y) (h2 : x' ≤ᵥ y') : x * x' ≤ᵥ y * y'

Alias of ValuativeRel.mul_vle_mul.

@[simp]

theorem ValuativeRel.mul_vle_mul_iff_left {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hz : 0 <ᵥ z) : x * z ≤ᵥ y * z ↔ x ≤ᵥ y

@[deprecated ValuativeRel.mul_vle_mul_iff_left (since := "2025-12-20")]

theorem ValuativeRel.mul_rel_mul_iff_left {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hz : 0 <ᵥ z) : x * z ≤ᵥ y * z ↔ x ≤ᵥ y

Alias of ValuativeRel.mul_vle_mul_iff_left.

@[simp]

theorem ValuativeRel.mul_vle_mul_iff_right {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hx : 0 <ᵥ x) : x * y ≤ᵥ x * z ↔ y ≤ᵥ z

@[deprecated ValuativeRel.mul_vle_mul_iff_right (since := "2025-12-20")]

theorem ValuativeRel.mul_rel_mul_iff_right {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hx : 0 <ᵥ x) : x * y ≤ᵥ x * z ↔ y ≤ᵥ z

Alias of ValuativeRel.mul_vle_mul_iff_right.

@[simp]

theorem ValuativeRel.mul_vlt_mul_iff_left {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hz : 0 <ᵥ z) : x * z <ᵥ y * z ↔ x <ᵥ y

theorem ValuativeRel.mul_vlt_mul_left {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hz : 0 <ᵥ z) : x <ᵥ y → x * z <ᵥ y * z

Alias of the reverse direction of ValuativeRel.mul_vlt_mul_iff_left.

@[deprecated ValuativeRel.mul_vlt_mul_left (since := "2026-01-06")]

theorem ValuativeRel.vlt_mul_right {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hz : 0 <ᵥ z) : x <ᵥ y → x * z <ᵥ y * z

Alias of the reverse direction of ValuativeRel.mul_vlt_mul_iff_left.

---

Alias of the reverse direction of ValuativeRel.mul_vlt_mul_iff_left.

@[deprecated ValuativeRel.mul_vlt_mul_iff_left (since := "2025-12-20")]

theorem ValuativeRel.mul_srel_mul_iff_left {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hz : 0 <ᵥ z) : x * z <ᵥ y * z ↔ x <ᵥ y

Alias of ValuativeRel.mul_vlt_mul_iff_left.

@[simp]

theorem ValuativeRel.mul_vlt_mul_iff_right {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hx : 0 <ᵥ x) : x * y <ᵥ x * z ↔ y <ᵥ z

theorem ValuativeRel.mul_vlt_mul_right {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hx : 0 <ᵥ x) : y <ᵥ z → x * y <ᵥ x * z

Alias of the reverse direction of ValuativeRel.mul_vlt_mul_iff_right.

@[deprecated ValuativeRel.mul_vlt_mul_right (since := "2026-01-06")]

theorem ValuativeRel.vlt_mul_left {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hx : 0 <ᵥ x) : y <ᵥ z → x * y <ᵥ x * z

Alias of the reverse direction of ValuativeRel.mul_vlt_mul_iff_right.

---

Alias of the reverse direction of ValuativeRel.mul_vlt_mul_iff_right.

@[deprecated ValuativeRel.mul_vlt_mul_iff_right (since := "2025-12-20")]

theorem ValuativeRel.mul_srel_mul_iff_right {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hx : 0 <ᵥ x) : x * y <ᵥ x * z ↔ y <ᵥ z

Alias of ValuativeRel.mul_vlt_mul_iff_right.

@[deprecated ValuativeRel.mul_vle_mul (since := "2025-11-04")]

theorem ValuativeRel.rel_mul {R : Type u_1} [CommRing R] [ValuativeRel R] {x x' y y' : R} (h1 : x ≤ᵥ y) (h2 : x' ≤ᵥ y') : x * x' ≤ᵥ y * y'

Alias of ValuativeRel.mul_vle_mul.

theorem ValuativeRel.mul_veq_mul {R : Type u_1} [CommRing R] [ValuativeRel R] {x x' y y' : R} (h1 : x =ᵥ y) (h2 : x' =ᵥ y') : x * x' =ᵥ y * y'

theorem ValuativeRel.vle_add_cases {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) : x + y ≤ᵥ x ∨ x + y ≤ᵥ y

@[deprecated ValuativeRel.vle_add_cases (since := "2025-12-20")]

theorem ValuativeRel.rel_add_cases {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) : x + y ≤ᵥ x ∨ x + y ≤ᵥ y

Alias of ValuativeRel.vle_add_cases.

@[simp]

theorem ValuativeRel.zero_vlt_mul {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (hx : 0 <ᵥ x) (hy : 0 <ᵥ y) : 0 <ᵥ x * y

@[deprecated ValuativeRel.zero_vlt_mul (since := "2025-12-20")]

theorem ValuativeRel.zero_srel_mul {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} (hx : 0 <ᵥ x) (hy : 0 <ᵥ y) : 0 <ᵥ x * y

Alias of ValuativeRel.zero_vlt_mul.

def ValuativeRel.posSubmonoid (R : Type u_1) [CommRing R] [ValuativeRel R] : Submonoid R

The submonoid of elements x : R whose valuation is positive.

Equations

• ValuativeRel.posSubmonoid R = { carrier := {x : R | 0 <ᵥ x}, mul_mem' := ⋯, one_mem' := ⋯ }

@[simp]

theorem ValuativeRel.zero_vlt_coe_posSubmonoid {R : Type u_1} [CommRing R] [ValuativeRel R] (x : ↥(posSubmonoid R)) : 0 <ᵥ ↑x

@[deprecated ValuativeRel.zero_vlt_coe_posSubmonoid (since := "2025-12-20")]

theorem ValuativeRel.zero_srel_coe_posSubmonoid {R : Type u_1} [CommRing R] [ValuativeRel R] (x : ↥(posSubmonoid R)) : 0 <ᵥ ↑x

Alias of ValuativeRel.zero_vlt_coe_posSubmonoid.

@[simp]

theorem ValuativeRel.posSubmonoid_def {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : x ∈ posSubmonoid R ↔ 0 <ᵥ x

theorem ValuativeRel.right_cancel_posSubmonoid {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) (u : ↥(posSubmonoid R)) : x * ↑u ≤ᵥ y * ↑u ↔ x ≤ᵥ y

theorem ValuativeRel.left_cancel_posSubmonoid {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) (u : ↥(posSubmonoid R)) : ↑u * x ≤ᵥ ↑u * y ↔ x ≤ᵥ y

@[simp]

theorem ValuativeRel.val_posSubmonoid_ne_zero {R : Type u_1} [CommRing R] [ValuativeRel R] (x : ↥(posSubmonoid R)) : ↑x ≠ 0

@[implicit_reducible]

def ValuativeRel.valueSetoid (R : Type u_1) [CommRing R] [ValuativeRel R] : Setoid (R × ↥(posSubmonoid R))

The setoid used to construct ValueGroupWithZero R.

Equations

• One or more equations did not get rendered due to their size.

def ValuativeRel.ValueGroupWithZero (R : Type u_1) [CommRing R] [ValuativeRel R] : Type u_1

The "canonical" value group-with-zero of a ring with a valuative relation.

Equations

• ValuativeRel.ValueGroupWithZero R = Quotient (ValuativeRel.valueSetoid R)

def ValuativeRel.ValueGroupWithZero.mk {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) (y : ↥(posSubmonoid R)) : ValueGroupWithZero R

Construct an element of the value group-with-zero from an element r : R and y : posSubmonoid R. This should be thought of as v r / v y.

Equations

• ValuativeRel.ValueGroupWithZero.mk x y = ⟦(x, y)⟧

theorem ValuativeRel.ValueGroupWithZero.sound {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} {t s : ↥(posSubmonoid R)} (h₁ : x * ↑s ≤ᵥ y * ↑t) (h₂ : y * ↑t ≤ᵥ x * ↑s) : ValueGroupWithZero.mk x t = ValueGroupWithZero.mk y s

theorem ValuativeRel.ValueGroupWithZero.exact {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} {t s : ↥(posSubmonoid R)} (h : ValueGroupWithZero.mk x t = ValueGroupWithZero.mk y s) : x * ↑s ≤ᵥ y * ↑t ∧ y * ↑t ≤ᵥ x * ↑s

theorem ValuativeRel.ValueGroupWithZero.ind {R : Type u_1} [CommRing R] [ValuativeRel R] {motive : ValueGroupWithZero R → Prop} (mk : ∀ (x : R) (y : ↥(posSubmonoid R)), motive (ValueGroupWithZero.mk x y)) (t : ValueGroupWithZero R) : motive t

def ValuativeRel.ValueGroupWithZero.lift {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → α) (hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) (t : ValueGroupWithZero R) : α

Lifts a function R → posSubmonoid R → α to the value group-with-zero of R.

Equations

• ValuativeRel.ValueGroupWithZero.lift f hf t = Quotient.lift (fun (x : R × ↥(ValuativeRel.posSubmonoid R)) => match x with | (x, y) => f x y) ⋯ t

@[simp]

theorem ValuativeRel.ValueGroupWithZero.lift_mk {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → α) (hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) (x : R) (y : ↥(posSubmonoid R)) : ValueGroupWithZero.lift f hf (ValueGroupWithZero.mk x y) = f x y

def ValuativeRel.ValueGroupWithZero.lift₂ {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → R → ↥(posSubmonoid R) → α) (hf : ∀ (x y z w : R) (t s u v : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → z * ↑u ≤ᵥ w * ↑v → w * ↑v ≤ᵥ z * ↑u → f x s z v = f y t w u) (t₁ t₂ : ValueGroupWithZero R) : α

Lifts a function R → posSubmonoid R → R → posSubmonoid R → α to the value group-with-zero of R.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ValuativeRel.ValueGroupWithZero.lift₂_mk {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → R → ↥(posSubmonoid R) → α) (hf : ∀ (x y z w : R) (t s u v : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → z * ↑u ≤ᵥ w * ↑v → w * ↑v ≤ᵥ z * ↑u → f x s z v = f y t w u) (x y : R) (z w : ↥(posSubmonoid R)) : ValueGroupWithZero.lift₂ f hf (ValueGroupWithZero.mk x z) (ValueGroupWithZero.mk y w) = f x z y w

theorem ValuativeRel.ValueGroupWithZero.mk_eq_mk {R : Type u_1} [CommRing R] [ValuativeRel R] {x y : R} {t s : ↥(posSubmonoid R)} : ValueGroupWithZero.mk x t = ValueGroupWithZero.mk y s ↔ x * ↑s ≤ᵥ y * ↑t ∧ y * ↑t ≤ᵥ x * ↑s

@[implicit_reducible]

instance ValuativeRel.instZeroValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : Zero (ValueGroupWithZero R)

Equations

• ValuativeRel.instZeroValueGroupWithZero = { zero := ValuativeRel.ValueGroupWithZero.mk 0 1 }

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_eq_zero {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) (y : ↥(posSubmonoid R)) : ValueGroupWithZero.mk x y = 0 ↔ x ≤ᵥ 0

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_zero {R : Type u_1} [CommRing R] [ValuativeRel R] (x : ↥(posSubmonoid R)) : ValueGroupWithZero.mk 0 x = 0

@[implicit_reducible]

instance ValuativeRel.instOneValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : One (ValueGroupWithZero R)

Equations

• ValuativeRel.instOneValueGroupWithZero = { one := ValuativeRel.ValueGroupWithZero.mk 1 1 }

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_self {R : Type u_1} [CommRing R] [ValuativeRel R] (x : ↥(posSubmonoid R)) : ValueGroupWithZero.mk (↑x) x = 1

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_one_one {R : Type u_1} [CommRing R] [ValuativeRel R] : ValueGroupWithZero.mk 1 1 = 1

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_eq_one {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) (y : ↥(posSubmonoid R)) : ValueGroupWithZero.mk x y = 1 ↔ x ≤ᵥ ↑y ∧ ↑y ≤ᵥ x

theorem ValuativeRel.ValueGroupWithZero.lift_zero {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → α) (hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) : ValueGroupWithZero.lift f hf 0 = f 0 1

@[simp]

theorem ValuativeRel.ValueGroupWithZero.lift_one {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → α) (hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) : ValueGroupWithZero.lift f hf 1 = f 1 1

@[implicit_reducible]

instance ValuativeRel.instMulValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : Mul (ValueGroupWithZero R)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_mul_mk {R : Type u_1} [CommRing R] [ValuativeRel R] (a b : R) (c d : ↥(posSubmonoid R)) : ValueGroupWithZero.mk a c * ValueGroupWithZero.mk b d = ValueGroupWithZero.mk (a * b) (c * d)

theorem ValuativeRel.ValueGroupWithZero.lift_mul {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Type u_2} [Mul α] (f : R → ↥(posSubmonoid R) → α) (hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) (hdist : ∀ (a b : R) (r s : ↥(posSubmonoid R)), f (a * b) (r * s) = f a r * f b s) (a b : ValueGroupWithZero R) : ValueGroupWithZero.lift f hf (a * b) = ValueGroupWithZero.lift f hf a * ValueGroupWithZero.lift f hf b

@[implicit_reducible]

instance ValuativeRel.instCommMonoidWithZeroValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : CommMonoidWithZero (ValueGroupWithZero R)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ValuativeRel.instLEValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : LE (ValueGroupWithZero R)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_le_mk {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) (t s : ↥(posSubmonoid R)) : ValueGroupWithZero.mk x t ≤ ValueGroupWithZero.mk y s ↔ x * ↑s ≤ᵥ y * ↑t

@[implicit_reducible]

noncomputable instance ValuativeRel.instLinearOrderValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : LinearOrder (ValueGroupWithZero R)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_lt_mk {R : Type u_1} [CommRing R] [ValuativeRel R] (x y : R) (t s : ↥(posSubmonoid R)) : ValueGroupWithZero.mk x t < ValueGroupWithZero.mk y s ↔ x * ↑s <ᵥ y * ↑t

@[simp]

theorem ValuativeRel.ValueGroupWithZero.mk_pos {R : Type u_1} [CommRing R] [ValuativeRel R] {x : R} {s : ↥(posSubmonoid R)} : 0 < ValueGroupWithZero.mk x s ↔ 0 <ᵥ x

@[implicit_reducible]

instance ValuativeRel.instBotValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : Bot (ValueGroupWithZero R)

Equations

• ValuativeRel.instBotValueGroupWithZero = { bot := 0 }

theorem ValuativeRel.ValueGroupWithZero.bot_eq_zero {R : Type u_1} [CommRing R] [ValuativeRel R] : ⊥ = 0

@[implicit_reducible]

instance ValuativeRel.instOrderBotValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : OrderBot (ValueGroupWithZero R)

Equations

• ValuativeRel.instOrderBotValueGroupWithZero = { toBot := ValuativeRel.instBotValueGroupWithZero, bot_le := ⋯ }

instance ValuativeRel.instIsOrderedMonoidValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : IsOrderedMonoid (ValueGroupWithZero R)

@[implicit_reducible]

noncomputable instance ValuativeRel.instInvValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : Inv (ValueGroupWithZero R)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ValuativeRel.ValueGroupWithZero.inv_mk {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) (y : ↥(posSubmonoid R)) (hx : ¬x ≤ᵥ 0) : (ValueGroupWithZero.mk x y)⁻¹ = ValueGroupWithZero.mk ↑y ⟨x, hx⟩

@[implicit_reducible]

noncomputable instance ValuativeRel.instLinearOrderedCommGroupWithZeroValueGroupWithZero {R : Type u_1} [CommRing R] [ValuativeRel R] : LinearOrderedCommGroupWithZero (ValueGroupWithZero R)

The value group-with-zero is a linearly ordered commutative group with zero.

Equations

• One or more equations did not get rendered due to their size.

def ValuativeRel.valuation (R : Type u_1) [CommRing R] [ValuativeRel R] : Valuation R (ValueGroupWithZero R)

The "canonical" valuation associated to a valuative relation.

Equations

• ValuativeRel.valuation R = { toFun := fun (r : R) => ValuativeRel.ValueGroupWithZero.mk r 1, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }

instance ValuativeRel.instCompatibleValueGroupWithZeroValuation {R : Type u_1} [CommRing R] [ValuativeRel R] : (valuation R).Compatible

@[simp]

theorem ValuativeRel.ValueGroupWithZero.lift_valuation {R : Type u_1} [CommRing R] [ValuativeRel R] {α : Sort u_2} (f : R → ↥(posSubmonoid R) → α) (hf : ∀ (x y : R) (t s : ↥(posSubmonoid R)), x * ↑t ≤ᵥ y * ↑s → y * ↑s ≤ᵥ x * ↑t → f x s = f y t) (x : R) : ValueGroupWithZero.lift f hf ((valuation R) x) = f x 1

theorem ValuativeRel.valuation_eq_zero_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {x : R} : (valuation R) x = 0 ↔ x ≤ᵥ 0

theorem ValuativeRel.valuation_posSubmonoid_ne_zero {R : Type u_1} [CommRing R] [ValuativeRel R] (x : ↥(posSubmonoid R)) : (valuation R) ↑x ≠ 0

theorem ValuativeRel.ValueGroupWithZero.mk_eq_div {R : Type u_1} [CommRing R] [ValuativeRel R] (r : R) (s : ↥(posSubmonoid R)) : ValueGroupWithZero.mk r s = (valuation R) r / (valuation R) ↑s

@[implicit_reducible]

def ValuativeRel.ofValuation {S : Type u_2} {Γ : Type u_3} [CommRing S] [LinearOrderedCommGroupWithZero Γ] (v : Valuation S Γ) : ValuativeRel S

Construct a valuative relation on a ring using a valuation.

Equations

• ValuativeRel.ofValuation v = { vle := fun (x y : S) => v x ≤ v y, vle_total := ⋯, vle_trans := ⋯, vle_add := ⋯, mul_vle_mul_left := ⋯, vle_mul_cancel := ⋯, not_vle_one_zero := ⋯ }

theorem Valuation.Compatible.ofValuation {S : Type u_2} {Γ : Type u_3} [CommRing S] [LinearOrderedCommGroupWithZero Γ] (v : Valuation S Γ) : v.Compatible

theorem ValuativeRel.isEquiv {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₁ : Type u_2} {Γ₂ : Type u_3} [LinearOrderedCommMonoidWithZero Γ₁] [LinearOrderedCommMonoidWithZero Γ₂] (v₁ : Valuation R Γ₁) (v₂ : Valuation R Γ₂) [v₁.Compatible] [v₂.Compatible] : v₁.IsEquiv v₂

theorem Valuation.vle_iff_le {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x y : R} : x ≤ᵥ y ↔ v x ≤ v y

@[deprecated Valuation.vle_iff_le (since := "2025-12-20")]

theorem Valuation.rel_iff_le {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x y : R} : x ≤ᵥ y ↔ v x ≤ v y

Alias of Valuation.vle_iff_le.

theorem Valuation.vlt_iff_lt {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x y : R} : x <ᵥ y ↔ v x < v y

@[deprecated Valuation.vlt_iff_lt (since := "2025-12-20")]

theorem Valuation.srel_iff_lt {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x y : R} : x <ᵥ y ↔ v x < v y

Alias of Valuation.vlt_iff_lt.

@[deprecated Valuation.vlt_iff_lt (since := "2025-10-09")]

theorem Valuation.Compatible.srel_iff_lt {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x y : R} : x <ᵥ y ↔ v x < v y

Alias of Valuation.vlt_iff_lt.

theorem Valuation.veq_iff_eq {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x y : R} : x =ᵥ y ↔ v x = v y

theorem Valuation.vle_one_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x : R} : x ≤ᵥ 1 ↔ v x ≤ 1

theorem Valuation.vlt_one_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x : R} : x <ᵥ 1 ↔ v x < 1

theorem Valuation.one_vle_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x : R} : 1 ≤ᵥ x ↔ 1 ≤ v x

theorem Valuation.one_vlt_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x : R} : 1 <ᵥ x ↔ 1 < v x

@[deprecated Valuation.vle_one_iff (since := "2025-12-20")]

theorem Valuation.rel_one_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x : R} : x ≤ᵥ 1 ↔ v x ≤ 1

Alias of Valuation.vle_one_iff.

@[deprecated Valuation.vlt_one_iff (since := "2025-12-20")]

theorem Valuation.srel_one_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x : R} : x <ᵥ 1 ↔ v x < 1

Alias of Valuation.vlt_one_iff.

@[deprecated Valuation.one_vle_iff (since := "2025-12-20")]

theorem Valuation.one_rel_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x : R} : 1 ≤ᵥ x ↔ 1 ≤ v x

Alias of Valuation.one_vle_iff.

@[deprecated Valuation.one_vlt_iff (since := "2025-12-20")]

theorem Valuation.one_srel_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] {x : R} : 1 <ᵥ x ↔ 1 < v x

Alias of Valuation.one_vlt_iff.

@[simp]

theorem Valuation.apply_posSubmonoid_ne_zero {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] (x : ↥(ValuativeRel.posSubmonoid R)) : v ↑x ≠ 0

@[simp]

theorem Valuation.apply_posSubmonoid_pos {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] (x : ↥(ValuativeRel.posSubmonoid R)) : 0 < v ↑x

def ValuativeRel.WithPreorder (R : Type u_1) : Type u_1

An alias for endowing a ring with a preorder defined as the valuative relation.

Equations

• ValuativeRel.WithPreorder R = R

@[implicit_reducible]

instance ValuativeRel.instCommRingWithPreorder {R : Type u_1} [CommRing R] : CommRing (WithPreorder R)

The ring instance on WithPreorder R arising from the ring structure on R.

Equations

• ValuativeRel.instCommRingWithPreorder = ValuativeRel.instCommRingWithPreorder._aux_1

@[implicit_reducible]

instance ValuativeRel.instPreorderWithPreorder {R : Type u_1} [CommRing R] [ValuativeRel R] : Preorder (WithPreorder R)

The preorder on WithPreorder R arising from the valuative relation on R.

Equations

• ValuativeRel.instPreorderWithPreorder = { le := fun (x y : R) => x ≤ᵥ y, lt := fun (x y : R) => x <ᵥ y, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }

@[implicit_reducible]

instance ValuativeRel.instWithPreorder {R : Type u_1} [CommRing R] [ValuativeRel R] : ValuativeRel (WithPreorder R)

The valuative relation on WithPreorder R arising from the valuative relation on R. This is defined as the preorder itself.

Equations

• One or more equations did not get rendered due to their size.

instance ValuativeRel.instValuativePreorderWithPreorder {R : Type u_1} [CommRing R] [ValuativeRel R] : ValuativePreorder (WithPreorder R)

def ValuativeRel.supp (R : Type u_1) [CommRing R] [ValuativeRel R] : Ideal R

The support of the valuation on R.

Equations

• ValuativeRel.supp R = { carrier := {x : R | x ≤ᵥ 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem ValuativeRel.supp_def {R : Type u_1} [CommRing R] [ValuativeRel R] (x : R) : x ∈ supp R ↔ x ≤ᵥ 0

theorem ValuativeRel.supp_eq_valuation_supp {R : Type u_1} [CommRing R] [ValuativeRel R] : supp R = (valuation R).supp

instance ValuativeRel.instIsPrimeSupp {R : Type u_1} [CommRing R] [ValuativeRel R] : (supp R).IsPrime

theorem ValuativeRel.vlt_of_vlt_of_vle {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c : R} (hab : a <ᵥ b) (hbc : b ≤ᵥ c) : a <ᵥ c

@[deprecated ValuativeRel.vlt_of_vlt_of_vle (since := "2025-12-20")]

theorem ValuativeRel.srel_of_srel_of_rel {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c : R} (hab : a <ᵥ b) (hbc : b ≤ᵥ c) : a <ᵥ c

Alias of ValuativeRel.vlt_of_vlt_of_vle.

theorem ValuativeRel.vlt.trans_vle {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c : R} (hab : a <ᵥ b) (hbc : b ≤ᵥ c) : a <ᵥ c

Alias of ValuativeRel.vlt_of_vlt_of_vle.

@[deprecated ValuativeRel.vlt.trans_vle (since := "2025-12-20")]

theorem ValuativeRel.SRel.trans_rel {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c : R} (hab : a <ᵥ b) (hbc : b ≤ᵥ c) : a <ᵥ c

Alias of ValuativeRel.vlt_of_vlt_of_vle.

---

Alias of ValuativeRel.vlt_of_vlt_of_vle.

theorem ValuativeRel.vlt_of_vle_of_vlt {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c : R} (hab : a ≤ᵥ b) (hbc : b <ᵥ c) : a <ᵥ c

@[deprecated ValuativeRel.mul_vlt_mul_iff_left (since := "2025-12-20")]

theorem ValuativeRel.srel_of_rel_of_srel {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hz : 0 <ᵥ z) : x * z <ᵥ y * z ↔ x <ᵥ y

Alias of ValuativeRel.mul_vlt_mul_iff_left.

theorem ValuativeRel.vle.trans_vlt {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c : R} (hab : a ≤ᵥ b) (hbc : b <ᵥ c) : a <ᵥ c

Alias of ValuativeRel.vlt_of_vle_of_vlt.

@[deprecated ValuativeRel.srel_of_rel_of_srel (since := "2025-12-20")]

theorem ValuativeRel.Rel.trans_srel {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hz : 0 <ᵥ z) : x * z <ᵥ y * z ↔ x <ᵥ y

Alias of ValuativeRel.mul_vlt_mul_iff_left.

---

Alias of ValuativeRel.mul_vlt_mul_iff_left.

theorem ValuativeRel.vlt.vle {R : Type u_2} [CommRing R] [ValuativeRel R] {a b : R} (hab : a <ᵥ b) : a ≤ᵥ b

@[deprecated ValuativeRel.vlt.vle (since := "2025-12-20")]

theorem ValuativeRel.SRel.rel {R : Type u_2} [CommRing R] [ValuativeRel R] {a b : R} (hab : a <ᵥ b) : a ≤ᵥ b

Alias of ValuativeRel.vlt.vle.

theorem ValuativeRel.vlt.trans {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c : R} (hab : a <ᵥ b) (hbc : b <ᵥ c) : a <ᵥ c

@[deprecated ValuativeRel.vlt.trans (since := "2025-12-20")]

theorem ValuativeRel.SRel.trans {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c : R} (hab : a <ᵥ b) (hbc : b <ᵥ c) : a <ᵥ c

Alias of ValuativeRel.vlt.trans.

@[deprecated ValuativeRel.mul_vle_mul_iff_left (since := "2026-01-06")]

theorem ValuativeRel.vle_mul_right_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hz : 0 <ᵥ z) : x * z ≤ᵥ y * z ↔ x ≤ᵥ y

Alias of ValuativeRel.mul_vle_mul_iff_left.

@[deprecated ValuativeRel.vle_mul_right_iff (since := "2025-12-20")]

theorem ValuativeRel.rel_mul_right_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hz : 0 <ᵥ z) : x * z ≤ᵥ y * z ↔ x ≤ᵥ y

Alias of ValuativeRel.mul_vle_mul_iff_left.

---

Alias of ValuativeRel.mul_vle_mul_iff_left.

@[deprecated ValuativeRel.mul_vle_mul_iff_right (since := "2026-01-06")]

theorem ValuativeRel.vle_mul_left_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hx : 0 <ᵥ x) : x * y ≤ᵥ x * z ↔ y ≤ᵥ z

Alias of ValuativeRel.mul_vle_mul_iff_right.

@[deprecated ValuativeRel.mul_vle_mul_iff_right (since := "2025-12-20")]

theorem ValuativeRel.rel_mul_left_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hx : 0 <ᵥ x) : x * y ≤ᵥ x * z ↔ y ≤ᵥ z

Alias of ValuativeRel.mul_vle_mul_iff_right.

@[deprecated ValuativeRel.mul_vlt_mul_iff_left (since := "2026-01-06")]

theorem ValuativeRel.vlt_mul_right_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hz : 0 <ᵥ z) : x * z <ᵥ y * z ↔ x <ᵥ y

Alias of ValuativeRel.mul_vlt_mul_iff_left.

@[deprecated ValuativeRel.mul_vlt_mul_iff_left (since := "2025-12-20")]

theorem ValuativeRel.srel_mul_right_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hz : 0 <ᵥ z) : x * z <ᵥ y * z ↔ x <ᵥ y

Alias of ValuativeRel.mul_vlt_mul_iff_left.

@[deprecated ValuativeRel.mul_vlt_mul_right (since := "2025-12-20")]

theorem ValuativeRel.srel_mul_right {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hx : 0 <ᵥ x) : y <ᵥ z → x * y <ᵥ x * z

Alias of the reverse direction of ValuativeRel.mul_vlt_mul_iff_right.

---

Alias of the reverse direction of ValuativeRel.mul_vlt_mul_iff_right.

@[deprecated ValuativeRel.mul_vlt_mul_iff_right (since := "2026-01-06")]

theorem ValuativeRel.vlt_mul_left_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hx : 0 <ᵥ x) : x * y <ᵥ x * z ↔ y <ᵥ z

Alias of ValuativeRel.mul_vlt_mul_iff_right.

@[deprecated ValuativeRel.mul_vlt_mul_iff_right (since := "2025-12-20")]

theorem ValuativeRel.srel_mul_left_iff {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hx : 0 <ᵥ x) : x * y <ᵥ x * z ↔ y <ᵥ z

Alias of ValuativeRel.mul_vlt_mul_iff_right.

@[deprecated ValuativeRel.mul_vlt_mul_right (since := "2025-12-20")]

theorem ValuativeRel.srel_mul_left {R : Type u_1} [CommRing R] [ValuativeRel R] {x y z : R} (hx : 0 <ᵥ x) : y <ᵥ z → x * y <ᵥ x * z

Alias of the reverse direction of ValuativeRel.mul_vlt_mul_iff_right.

---

Alias of the reverse direction of ValuativeRel.mul_vlt_mul_iff_right.

theorem ValuativeRel.mul_vlt_mul_of_vlt_of_vle {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c d : R} (hab : a <ᵥ b) (hcd : c ≤ᵥ d) (hd : 0 <ᵥ d) : a * c <ᵥ b * d

@[deprecated ValuativeRel.mul_vlt_mul_of_vlt_of_vle (since := "2025-12-20")]

theorem ValuativeRel.mul_srel_mul_of_srel_of_rel {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c d : R} (hab : a <ᵥ b) (hcd : c ≤ᵥ d) (hd : 0 <ᵥ d) : a * c <ᵥ b * d

Alias of ValuativeRel.mul_vlt_mul_of_vlt_of_vle.

theorem ValuativeRel.mul_vlt_mul_of_vle_of_vlt {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c d : R} (hab : a ≤ᵥ b) (hcd : c <ᵥ d) (ha : 0 <ᵥ a) : a * c <ᵥ b * d

@[deprecated ValuativeRel.mul_vlt_mul_of_vle_of_vlt (since := "2025-12-20")]

theorem ValuativeRel.mul_srel_mul_of_rel_of_srel {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c d : R} (hab : a ≤ᵥ b) (hcd : c <ᵥ d) (ha : 0 <ᵥ a) : a * c <ᵥ b * d

Alias of ValuativeRel.mul_vlt_mul_of_vle_of_vlt.

theorem ValuativeRel.mul_vlt_mul {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c d : R} (hab : a <ᵥ b) (hcd : c <ᵥ d) : a * c <ᵥ b * d

@[deprecated ValuativeRel.mul_vlt_mul (since := "2025-12-20")]

theorem ValuativeRel.mul_srel_mul {R : Type u_2} [CommRing R] [ValuativeRel R] {a b c d : R} (hab : a <ᵥ b) (hcd : c <ᵥ d) : a * c <ᵥ b * d

Alias of ValuativeRel.mul_vlt_mul.

theorem ValuativeRel.pow_vle_pow {R : Type u_2} [CommRing R] [ValuativeRel R] {a b : R} (hab : a ≤ᵥ b) (n : ℕ) : a ^ n ≤ᵥ b ^ n

@[deprecated ValuativeRel.pow_vle_pow (since := "2025-12-20")]

theorem ValuativeRel.pow_rel_pow {R : Type u_2} [CommRing R] [ValuativeRel R] {a b : R} (hab : a ≤ᵥ b) (n : ℕ) : a ^ n ≤ᵥ b ^ n

Alias of ValuativeRel.pow_vle_pow.

theorem ValuativeRel.pow_vlt_pow {R : Type u_2} [CommRing R] [ValuativeRel R] {a b : R} (hab : a <ᵥ b) {n : ℕ} (hn : n ≠ 0) : a ^ n <ᵥ b ^ n

@[deprecated ValuativeRel.pow_vlt_pow (since := "2025-12-20")]

theorem ValuativeRel.pow_srel_pow {R : Type u_2} [CommRing R] [ValuativeRel R] {a b : R} (hab : a <ᵥ b) {n : ℕ} (hn : n ≠ 0) : a ^ n <ᵥ b ^ n

Alias of ValuativeRel.pow_vlt_pow.

theorem ValuativeRel.pow_vle_pow_of_vle_one {R : Type u_2} [CommRing R] [ValuativeRel R] {a : R} (ha : a ≤ᵥ 1) {n m : ℕ} (hnm : n ≤ m) : a ^ m ≤ᵥ a ^ n

@[deprecated ValuativeRel.pow_vle_pow_of_vle_one (since := "2025-12-20")]

theorem ValuativeRel.pow_rel_pow_of_rel_one {R : Type u_2} [CommRing R] [ValuativeRel R] {a : R} (ha : a ≤ᵥ 1) {n m : ℕ} (hnm : n ≤ m) : a ^ m ≤ᵥ a ^ n

Alias of ValuativeRel.pow_vle_pow_of_vle_one.

theorem ValuativeRel.pow_vle_pow_of_one_vle {R : Type u_2} [CommRing R] [ValuativeRel R] {a : R} (ha : 1 ≤ᵥ a) {n m : ℕ} (hnm : n ≤ m) : a ^ n ≤ᵥ a ^ m

@[deprecated ValuativeRel.pow_vle_pow_of_one_vle (since := "2025-12-20")]

theorem ValuativeRel.pow_rel_pow_of_one_rel {R : Type u_2} [CommRing R] [ValuativeRel R] {a : R} (ha : 1 ≤ᵥ a) {n m : ℕ} (hnm : n ≤ m) : a ^ n ≤ᵥ a ^ m

Alias of ValuativeRel.pow_vle_pow_of_one_vle.

@[simp]

theorem ValuativeRel.vle_zero_iff {K : Type u_2} [Field K] [ValuativeRel K] {a : K} : a ≤ᵥ 0 ↔ a = 0

@[deprecated ValuativeRel.vle_zero_iff (since := "2025-12-20")]

theorem ValuativeRel.rel_zero_iff {K : Type u_2} [Field K] [ValuativeRel K] {a : K} : a ≤ᵥ 0 ↔ a = 0

Alias of ValuativeRel.vle_zero_iff.

@[simp]

theorem ValuativeRel.zero_vlt_iff {K : Type u_2} [Field K] [ValuativeRel K] {a : K} : 0 <ᵥ a ↔ a ≠ 0

@[deprecated ValuativeRel.zero_vlt_iff (since := "2025-12-20")]

theorem ValuativeRel.zero_srel_iff {K : Type u_2} [Field K] [ValuativeRel K] {a : K} : 0 <ᵥ a ↔ a ≠ 0

Alias of ValuativeRel.zero_vlt_iff.

@[simp]

theorem ValuativeRel.zero_veq_iff {K : Type u_2} [Field K] [ValuativeRel K] {a : K} : a =ᵥ 0 ↔ a = 0

@[simp]

theorem ValuativeRel.veq_zero_iff {K : Type u_2} [Field K] [ValuativeRel K] {a : K} : 0 =ᵥ a ↔ 0 = a

theorem ValuativeRel.vle_div_iff {K : Type u_2} [Field K] [ValuativeRel K] {a b c : K} (hc : c ≠ 0) : a ≤ᵥ b / c ↔ a * c ≤ᵥ b

@[deprecated ValuativeRel.vle_div_iff (since := "2025-12-20")]

theorem ValuativeRel.rel_div_iff {K : Type u_2} [Field K] [ValuativeRel K] {a b c : K} (hc : c ≠ 0) : a ≤ᵥ b / c ↔ a * c ≤ᵥ b

Alias of ValuativeRel.vle_div_iff.

theorem ValuativeRel.div_vle_iff {K : Type u_2} [Field K] [ValuativeRel K] {a b c : K} (hc : c ≠ 0) : a / c ≤ᵥ b ↔ a ≤ᵥ b * c

@[deprecated ValuativeRel.div_vle_iff (since := "2025-12-20")]

theorem ValuativeRel.div_rel_iff {K : Type u_2} [Field K] [ValuativeRel K] {a b c : K} (hc : c ≠ 0) : a / c ≤ᵥ b ↔ a ≤ᵥ b * c

Alias of ValuativeRel.div_vle_iff.

theorem ValuativeRel.one_vle_div_iff {K : Type u_2} [Field K] [ValuativeRel K] {a b : K} (hb : b ≠ 0) : 1 ≤ᵥ a / b ↔ b ≤ᵥ a

@[deprecated ValuativeRel.one_vle_div_iff (since := "2025-12-20")]

theorem ValuativeRel.one_rel_div_iff {K : Type u_2} [Field K] [ValuativeRel K] {a b : K} (hb : b ≠ 0) : 1 ≤ᵥ a / b ↔ b ≤ᵥ a

Alias of ValuativeRel.one_vle_div_iff.

theorem ValuativeRel.div_vle_one_iff {K : Type u_2} [Field K] [ValuativeRel K] {a b : K} (hb : b ≠ 0) : a / b ≤ᵥ 1 ↔ a ≤ᵥ b

@[deprecated ValuativeRel.div_vle_one_iff (since := "2025-12-20")]

theorem ValuativeRel.div_rel_one_iff {K : Type u_2} [Field K] [ValuativeRel K] {a b : K} (hb : b ≠ 0) : a / b ≤ᵥ 1 ↔ a ≤ᵥ b

Alias of ValuativeRel.div_vle_one_iff.

theorem ValuativeRel.one_vle_inv {K : Type u_2} [Field K] [ValuativeRel K] {x : K} (hx : x ≠ 0) : 1 ≤ᵥ x⁻¹ ↔ x ≤ᵥ 1

@[deprecated ValuativeRel.one_vle_inv (since := "2025-12-20")]

theorem ValuativeRel.one_rel_inv {K : Type u_2} [Field K] [ValuativeRel K] {x : K} (hx : x ≠ 0) : 1 ≤ᵥ x⁻¹ ↔ x ≤ᵥ 1

Alias of ValuativeRel.one_vle_inv.

theorem ValuativeRel.inv_vle_one {K : Type u_2} [Field K] [ValuativeRel K] {x : K} (hx : x ≠ 0) : x⁻¹ ≤ᵥ 1 ↔ 1 ≤ᵥ x

@[deprecated ValuativeRel.inv_vle_one (since := "2025-12-20")]

theorem ValuativeRel.inv_rel_one {K : Type u_2} [Field K] [ValuativeRel K] {x : K} (hx : x ≠ 0) : x⁻¹ ≤ᵥ 1 ↔ 1 ≤ᵥ x

Alias of ValuativeRel.inv_vle_one.

theorem ValuativeRel.inv_vlt_one {K : Type u_2} [Field K] [ValuativeRel K] {x : K} (hx : x ≠ 0) : x⁻¹ <ᵥ 1 ↔ 1 <ᵥ x

@[deprecated ValuativeRel.inv_vlt_one (since := "2025-12-20")]

theorem ValuativeRel.inv_srel_one {K : Type u_2} [Field K] [ValuativeRel K] {x : K} (hx : x ≠ 0) : x⁻¹ <ᵥ 1 ↔ 1 <ᵥ x

Alias of ValuativeRel.inv_vlt_one.

theorem ValuativeRel.one_vlt_inv {K : Type u_2} [Field K] [ValuativeRel K] {x : K} (hx : x ≠ 0) : 1 <ᵥ x⁻¹ ↔ x <ᵥ 1

@[deprecated ValuativeRel.one_vlt_inv (since := "2025-12-20")]

theorem ValuativeRel.one_srel_inv {K : Type u_2} [Field K] [ValuativeRel K] {x : K} (hx : x ≠ 0) : 1 <ᵥ x⁻¹ ↔ x <ᵥ 1

Alias of ValuativeRel.one_vlt_inv.

structure ValuativeRel.RankLeOneStruct (R : Type u_1) [CommRing R] [ValuativeRel R] : Type u_1

An auxiliary structure used to define IsRankLeOne.

• emb : ValueGroupWithZero R →*₀ NNReal

  The embedding of the value group-with-zero into the nonnegative reals.

• strictMono : StrictMono ⇑self.emb

class ValuativeRel.IsRankLeOne (R : Type u_1) [CommRing R] [ValuativeRel R] : Prop

We say that a ring with a valuative relation is of rank one if there exists a strictly monotone embedding of the "canonical" value group-with-zero into the nonnegative reals, and the image of this embedding contains some element different from 0 and 1.

• nonempty : Nonempty (RankLeOneStruct R)

class ValuativeRel.IsNontrivial (R : Type u_1) [CommRing R] [ValuativeRel R] : Prop

We say that a valuative relation on a ring is nontrivial if the value group-with-zero is nontrivial, meaning that it has an element which is different from 0 and 1.

• condition : ∃ (γ : ValueGroupWithZero R), γ ≠ 0 ∧ γ ≠ 1

theorem ValuativeRel.IsNontrivial.exists_lt_one {R : Type u_1} [CommRing R] [ValuativeRel R] [IsNontrivial R] : ∃ (γ : ValueGroupWithZero R), 0 < γ ∧ γ < 1

theorem ValuativeRel.isNontrivial_iff_nontrivial_units {R : Type u_1} [CommRing R] [ValuativeRel R] : IsNontrivial R ↔ Nontrivial (ValueGroupWithZero R)ˣ

theorem ValuativeRel.isNontrivial_iff_isNontrivial {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀) [v.Compatible] : IsNontrivial R ↔ v.IsNontrivial

instance ValuativeRel.instIsNontrivialOfIsNontrivialOfCompatible {R : Type u_1} [CommRing R] [ValuativeRel R] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] [IsNontrivial R] (v : Valuation R Γ₀) [v.Compatible] : v.IsNontrivial

theorem ValuativeRel.ValueGroupWithZero.mk_eq_valuation {K : Type u_2} [Field K] [ValuativeRel K] (x : K) (y : ↥(posSubmonoid K)) : ValueGroupWithZero.mk x y = (valuation K) (x / ↑y)

theorem ValuativeRel.exists_valuation_div_valuation_eq {R : Type u_1} [CommRing R] [ValuativeRel R] (γ : ValueGroupWithZero R) : ∃ (a : R) (b : ↥(posSubmonoid R)), (valuation R) a / (valuation R) ↑b = γ

theorem ValuativeRel.exists_valuation_posSubmonoid_div_valuation_posSubmonoid_eq {R : Type u_1} [CommRing R] [ValuativeRel R] (γ : (ValueGroupWithZero R)ˣ) : ∃ (a : ↥(posSubmonoid R)) (b : ↥(posSubmonoid R)), (valuation R) ↑a / (valuation R) ↑b = ↑γ

theorem ValuativeRel.valuation_surjective {K : Type u_2} [Field K] [ValuativeRel K] : Function.Surjective ⇑(valuation K)

class ValuativeRel.IsDiscrete (R : Type u_1) [CommRing R] [ValuativeRel R] : Prop

A ring with a valuative relation is discrete if its value group-with-zero has a maximal element < 1.

• has_maximal_element : ∃ γ < 1, ∀ δ < 1, δ ≤ γ

noncomputable def ValuativeRel.uniformizer (R : Type u_1) [CommRing R] [ValuativeRel R] [IsDiscrete R] : ValueGroupWithZero R

The maximal element that is < 1 in the value group of a discrete valuation.

Equations

• ValuativeRel.uniformizer R = ⋯.choose

theorem ValuativeRel.uniformizer_lt_one {R : Type u_1} [CommRing R] [ValuativeRel R] [IsDiscrete R] : uniformizer R < 1

theorem ValuativeRel.le_uniformizer_iff {R : Type u_1} [CommRing R] [ValuativeRel R] [IsDiscrete R] {a : ValueGroupWithZero R} : a ≤ uniformizer R ↔ a < 1

theorem ValuativeRel.uniformizer_pos {R : Type u_1} [CommRing R] [ValuativeRel R] [IsDiscrete R] [IsNontrivial R] : 0 < uniformizer R

@[simp]

theorem ValuativeRel.uniformizer_ne_zero {R : Type u_1} [CommRing R] [ValuativeRel R] [IsDiscrete R] [IsNontrivial R] : uniformizer R ≠ 0

theorem ValuativeRel.uniformizer_inv_le_iff {R : Type u_1} [CommRing R] [ValuativeRel R] [IsDiscrete R] [IsNontrivial R] {a : ValueGroupWithZero R} : (uniformizer R)⁻¹ ≤ a ↔ 1 < a

noncomputable def ValuativeRel.ValueGroupWithZero.embed {R : Type u_2} {Γ : Type u_3} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [v.Compatible] : ValueGroupWithZero R →*₀ MonoidWithZeroHom.ValueGroup₀ v

The ValueGroupWithZero R is the "minimal" value group (with zero) among all value groups of valuations that are compatible with the valuative relation, in the sense that it is canonically isomorphic to the subgroup (with zero) generated by v '' R for any compatible v. ValueGroupWithZero.embed v is exactly this isomorphism map; it will later be upgraded to ValueGroupWithZero.orderMonoidIso v.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ValuativeRel.ValueGroupWithZero.embed_mk {R : Type u_2} {Γ : Type u_3} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [v.Compatible] (x : R) (s : ↥(posSubmonoid R)) : (embed v) (ValueGroupWithZero.mk x s) = (MonoidWithZeroHom.ValueGroup₀.restrict₀ v) x / (MonoidWithZeroHom.ValueGroup₀.restrict₀ v) ↑s

The element .mk x s in ValueGroupWithZero R is sent to v x / v s in the image group of v.

@[simp]

theorem ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀ {R : Type u_2} {Γ : Type u_3} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [v.Compatible] (x : R) : (embed v) ((valuation R) x) = (MonoidWithZeroHom.ValueGroup₀.restrict₀ v) x

The triangle in the following diagram is commutative:

      restrict₀ v                embedding
    R –––––––––––> ValueGroup₀ v –––––––––> Γ
    │                ∧
    │               /
    │              / embed v
    ∨             /
ValueGroupWithZero R

where the first row is the map v factored through its image group (with zero) in Γ.

@[simp]

theorem ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq {R : Type u_2} [CommRing R] [ValuativeRel R] (γ : ValueGroupWithZero R) : MonoidWithZeroHom.ValueGroup₀.embedding ((embed (valuation R)) γ) = γ

When v is valuation R, in the following commutative diagram where the first row is the map v factored through its image group (with zero),

                                 embedding
    R –––––––––––> ValueGroup₀ v –––––-–––> ValueGroupWithZero R
    │                ∧
    │               /
    │              / embed v
    ∨             /
ValueGroupWithZero R

the map from ValueGroupWithZero R to itself is identity.

theorem ValuativeRel.ValueGroupWithZero.embed_strictMono {R : Type u_2} {Γ : Type u_3} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [v.Compatible] : StrictMono ⇑(embed v)

The map embed v is strictly monotone.

@[simp]

theorem ValuativeRel.ValueGroupWithZero.orderMonoidIso_embed {R : Type u_2} {Γ : Type u_3} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [v.Compatible] {Γ' : Type u_4} [LinearOrderedCommGroupWithZero Γ'] (w : Valuation R Γ') [w.Compatible] (x : ValueGroupWithZero R) (h : w.IsEquiv v) : h.orderMonoidIso ((embed w) x) = (embed v) x

When we have h : w.IsEquiv v, the image group (with zero) of v is isomorphic to that of w via h.orderMonoidIso. Then the following diagram is commutative:

              ValueGroup₀ w
                ∧      |
       embed w /       |
              /        |
ValueGroupWithZero R   | h.orderMonoidIso
              \        |
       embed v \       |
                ∨      ∨
              ValueGroup₀ v

noncomputable def ValuativeRel.ValueGroupWithZero.orderMonoidIso {R : Type u_2} {Γ : Type u_3} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [v.Compatible] : ValueGroupWithZero R ≃*o MonoidWithZeroHom.ValueGroup₀ v

If a valuation v is compatible with the valuative relation, then ValueGroupWithZero R is isomorphic to the image group (with zero) of v as an ordered group with zero.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ValuativeRel.ValueGroupWithZero.orderMonoidIso_mk {R : Type u_2} {Γ : Type u_3} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [v.Compatible] (x : R) (s : ↥(posSubmonoid R)) : (orderMonoidIso v) (ValueGroupWithZero.mk x s) = (MonoidWithZeroHom.ValueGroup₀.restrict₀ v) x / (MonoidWithZeroHom.ValueGroup₀.restrict₀ v) ↑s

This is the same as ValuativeRel.ValueGroupWithZero.embed_mk, where embed is upgraded to orderMonoidIso.

@[simp]

theorem ValuativeRel.ValueGroupWithZero.orderMonoidIso_valuation_eq_restrict₀ {R : Type u_2} {Γ : Type u_3} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [v.Compatible] (x : R) : (orderMonoidIso v) ((valuation R) x) = (MonoidWithZeroHom.ValueGroup₀.restrict₀ v) x

This is the same as ValuativeRel.ValueGroupWithZero.embed_valuation_eq_restrict₀, where embed is upgraded to orderMonoidIso.

@[simp]

theorem ValuativeRel.ValueGroupWithZero.embedding_orderMonoidIso_valuation_eq {R : Type u_2} [CommRing R] [ValuativeRel R] (γ : ValueGroupWithZero R) : MonoidWithZeroHom.ValueGroup₀.embedding ((orderMonoidIso (valuation R)) γ) = γ

This is the same as ValuativeRel.ValueGroupWithZero.embedding_embed_valuation_eq, where embed is upgraded to orderMonoidIso.

theorem ValuativeRel.ValueGroupWithZero.orderMonoidIso_strictMono {R : Type u_2} {Γ : Type u_3} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [v.Compatible] : StrictMono ⇑(orderMonoidIso v)

The map orderMonoidIso v is strictly monotone.

theorem ValuativeRel.ValueGroupWithZero.leftInverse_embedding_orderMonoidIso {R : Type u_2} [CommRing R] [ValuativeRel R] : Function.LeftInverse ⇑MonoidWithZeroHom.ValueGroup₀.embedding ⇑(orderMonoidIso (valuation R))

The map embedding ∘ orderMonoidIso (valuation R)) is identity.

@[deprecated "use ValueGroupWithZero.embed (valuation R) instead" (since := "2026-03-17")]

noncomputable def ValuativeRel.ValueGroupWithZero.valueGroupWithZero_equiv_valueGroup₀ {R : Type u_2} [CommRing R] [ValuativeRel R] : ValueGroupWithZero R ≃*o MonoidWithZeroHom.ValueGroup₀ (valuation R)

The isomorphism between ValueGroupWithZero R and ValueGroup₀ (valuation R).

Equations

• ValuativeRel.ValueGroupWithZero.valueGroupWithZero_equiv_valueGroup₀ = ValuativeRel.ValueGroupWithZero.orderMonoidIso (ValuativeRel.valuation R)

@[simp]

theorem ValuativeRel.valuation_lt_symm_orderMonoidIso {R : Type u_2} {Γ : Type u_3} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [v.Compatible] (γ : MonoidWithZeroHom.ValueGroup₀ v) (x : R) : (valuation R) x < (ValueGroupWithZero.orderMonoidIso v).symm γ ↔ v.restrict x < γ

@[simp]

theorem ValuativeRel.restrict_lt_orderMonoidIso {R : Type u_2} {Γ : Type u_3} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] (v : Valuation R Γ) [v.Compatible] (γ : ValueGroupWithZero R) (x : R) : v.restrict x < (ValueGroupWithZero.orderMonoidIso v) γ ↔ (valuation R) x < γ

theorem ValuativeRel.one_apply_posSubmonoid {R : Type u_2} {Γ : Type u_3} [CommRing R] [ValuativeRel R] [LinearOrderedCommGroupWithZero Γ] [Nontrivial R] [NoZeroDivisors R] [DecidablePred fun (x : R) => x = 0] (x : ↥(posSubmonoid R)) : 1 ↑x = 1

For any x ∈ posSubmonoid R, the trivial valuation 1 : Valuation R Γ sends x to 1. In fact, this is true for any x ≠ 0. This lemma is a special case useful for shorthand of x ∈ posSubmonoid R → x ≠ 0.

class ValuativeExtension (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] : Prop

If B is an A algebra and both A and B have valuative relations, we say that B|A is a valuative extension if the valuative relation on A is induced by the one on B.

• vle_iff_vle (a b : A) : (algebraMap A B) a ≤ᵥ (algebraMap A B) b ↔ a ≤ᵥ b

theorem ValuativeExtension.vlt_iff_vlt {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] {a b : A} : (algebraMap A B) a <ᵥ (algebraMap A B) b ↔ a <ᵥ b

@[deprecated ValuativeExtension.vlt_iff_vlt (since := "2025-12-20")]

theorem ValuativeExtension.srel_iff_srel {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] {a b : A} : (algebraMap A B) a <ᵥ (algebraMap A B) b ↔ a <ᵥ b

Alias of ValuativeExtension.vlt_iff_vlt.

def ValuativeExtension.mapPosSubmonoid (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] : ↥(ValuativeRel.posSubmonoid A) →* ↥(ValuativeRel.posSubmonoid B)

The morphism of posSubmonoids associated to an algebra map. This is used in constructing ValuativeExtension.mapValueGroupWithZero.

Equations

• ValuativeExtension.mapPosSubmonoid A B = { toFun := fun (x : ↥(ValuativeRel.posSubmonoid A)) => match x with | ⟨a, ha⟩ => ⟨(algebraMap A B) a, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem ValuativeExtension.mapPosSubmonoid_apply_coe (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] (x✝ : ↥(ValuativeRel.posSubmonoid A)) : ↑((mapPosSubmonoid A B) x✝) = (algebraMap A B) ↑x✝

instance ValuativeExtension.compatible_comap (A : Type u_1) {B : Type u_2} [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] {Γ : Type u_3} [LinearOrderedCommMonoidWithZero Γ] (w : Valuation B Γ) [w.Compatible] : (Valuation.comap (algebraMap A B) w).Compatible

noncomputable def ValuativeExtension.mapValueGroupWithZero (A : Type u_1) (B : Type u_2) [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] : ValuativeRel.ValueGroupWithZero A →*₀ ValuativeRel.ValueGroupWithZero B

The map on value groups-with-zero associated to the structure morphism of an algebra.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem ValuativeExtension.mapValueGroupWithZero_mk {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] (r : A) (s : ↥(ValuativeRel.posSubmonoid A)) : (mapValueGroupWithZero A B) (ValuativeRel.ValueGroupWithZero.mk r s) = ValuativeRel.ValueGroupWithZero.mk ((algebraMap A B) r) ((mapPosSubmonoid A B) s)

@[simp]

theorem ValuativeExtension.mapValueGroupWithZero_valuation {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] (a : A) : (mapValueGroupWithZero A B) ((ValuativeRel.valuation A) a) = (ValuativeRel.valuation B) ((algebraMap A B) a)

theorem ValuativeExtension.mapValueGroupWithZero_strictMono {A : Type u_1} {B : Type u_2} [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] : StrictMono ⇑(mapValueGroupWithZero A B)

theorem ValuativeRel.IsRankLeOne.of_valuativeExtension {A : Type u_1} (B : Type u_2) [CommRing A] [CommRing B] [ValuativeRel A] [ValuativeRel B] [Algebra A B] [ValuativeExtension A B] [IsRankLeOne B] : IsRankLeOne A

instance ValuativeRel.instMulArchimedeanValueGroupWithZeroOfIsRankLeOne {R : Type u_1} [CommRing R] [ValuativeRel R] [IsRankLeOne R] : MulArchimedean (ValueGroupWithZero R)

Any rank-at-most-one valuation has a mul-archimedean value group. The converse (for any compatible valuation) is ValuativeRel.isRankLeOne_iff_mulArchimedean which is in a later file since it requires a larger theory of reals.