English
Let R be a commutative ring with a valuative relation. For any x, y in R and t, s in the positive submonoid of R, if the two valued elements mk(x, t) and mk(y, s) are equal, then x s and y t are mutually valuatively bounded; i.e., x s ≤ᵥ y t and y t ≤ᵥ x s.
Русский
Пусть R — коммутативное кольцо с оценивающей связью. Для любых x, y ∈ R и t, s ∈ posSubmonoid(R) равенство mk(x, t) = mk(y, s) в группе значений подразумевает, что x s и y t взаимно ограничены по valuative-отношению: x s ≤ᵥ y t и y t ≤ᵥ x s.
LaTeX
$$$\mathrm{ValueGroupWithZero.mk} \, x \, t = \mathrm{ValueGroupWithZero.mk} \, y \, s \Rightarrow x s \le_{\mathrm{v}} y t \wedge y t \le_{\mathrm{v}} x s$$$
Lean4
protected theorem exact {x y : R} {t s : posSubmonoid R} (h : ValueGroupWithZero.mk x t = ValueGroupWithZero.mk y s) :
x * s ≤ᵥ y * t ∧ y * t ≤ᵥ x * s :=
Quotient.exact h
