English
For any a,b in ValueGroup(A,K), either a ≤ b or b ≤ a.
Русский
Для любых a,b в ValueGroup(A,K) верно: либо a ≤ b, либо b ≤ a.
LaTeX
$$$\forall a,b \in \mathrm{ValueGroup}(A,K),\; a \le b \;\lor\; b \le a$$$
Lean4
protected theorem le_total (a b : ValueGroup A K) : a ≤ b ∨ b ≤ a :=
by
rcases a with ⟨a⟩; rcases b with ⟨b⟩
obtain ⟨xa, ya, hya, rfl⟩ : ∃ a b : A, _ := IsFractionRing.div_surjective a
obtain ⟨xb, yb, hyb, rfl⟩ : ∃ a b : A, _ := IsFractionRing.div_surjective b
have : (algebraMap A K) ya ≠ 0 := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hya
have : (algebraMap A K) yb ≠ 0 := IsFractionRing.to_map_ne_zero_of_mem_nonZeroDivisors hyb
obtain ⟨c, h | h⟩ := ValuationRing.cond (xa * yb) (xb * ya)
· right
use c
rw [Algebra.smul_def]
field_simp
simp only [← RingHom.map_mul]; congr 1; linear_combination h
· left
use c
rw [Algebra.smul_def]
field_simp
simp only [← RingHom.map_mul]; congr 1; linear_combination h
