instLEValueGroup — Mathlib

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])

Похожие утверждения