English
ValueGroup(A,K) is endowed with a linear order.
Русский
ValueGroup(A,K) наделён линейным порядком.
LaTeX
$$$\mathrm{ValueGroup}(A,K) \text{ is a linear order.}$$$
Lean4
noncomputable instance linearOrder : LinearOrder (ValueGroup A K)
where
le_refl := by rintro ⟨⟩; use 1; rw [one_smul]
le_trans := by rintro ⟨a⟩ ⟨b⟩ ⟨c⟩ ⟨e, rfl⟩ ⟨f, rfl⟩; use e * f; rw [mul_smul]
le_antisymm := by
rintro ⟨a⟩ ⟨b⟩ ⟨e, rfl⟩ ⟨f, hf⟩
by_cases hb : b = 0; · simp [hb]
have : IsUnit e := by
apply isUnit_of_dvd_one
use f
rw [mul_comm]
rw [← mul_smul, Algebra.smul_def] at hf
nth_rw 2 [← one_mul b] at hf
rw [← (algebraMap A K).map_one] at hf
exact IsFractionRing.injective _ _ (mul_right_cancel₀ hb hf).symm
apply Quotient.sound'
exact ⟨this.unit, rfl⟩
le_total := ValuationRing.le_total _ _
toDecidableLE := Classical.decRel _
