English
There is a linear order on ValueGroup(A,K) defined by a ≤ b iff there exists c ∈ A with c·b = a.
Русский
На ValueGroup(A,K) вводится линейный порядок, заданный как a ≤ b если существует c ∈ A такое что c·b = a.
LaTeX
$$$\exists \le: \mathrm{ValueGroup}(A,K) \times \mathrm{ValueGroup}(A,K) \to \{\text{Bool}\}$ с определением $a \le b \iff \exists c\in A,\; c\cdot b = a$$$
Lean4
instance : LE (ValueGroup A K) :=
LE.mk fun x y =>
Quotient.liftOn₂' x y (fun a b => ∃ c : A, c • b = a)
(by
rintro _ _ a b ⟨c, rfl⟩ ⟨d, rfl⟩; ext
constructor
· rintro ⟨e, he⟩; use (c⁻¹ : Aˣ) * e * d
apply_fun fun t => c⁻¹ • t at he
simpa [mul_smul] using he
· rintro ⟨e, he⟩; dsimp
use c * e * (d⁻¹ : Aˣ)
simp_rw [Units.smul_def, ← he, mul_smul]
rw [← mul_smul _ _ b, Units.inv_mul, one_smul])