instInvValueGroupWithZero — Mathlib

Lean4

instance : Inv (ValueGroupWithZero R) where
  inv :=
    ValueGroupWithZero.lift (fun x s => by classical exact if h : x ≤ᵥ 0 then 0 else .mk s ⟨x, h⟩) <|
      by
      intro x y t s h₁ h₂
      by_cases hx : x ≤ᵥ 0 <;> by_cases hy : y ≤ᵥ 0
      · simp [hx, hy]
      · absurd hy
        apply rel_mul_cancel s.prop
        simpa using rel_trans h₂ (rel_mul_right (t : R) hx)
      · absurd hx
        apply rel_mul_cancel t.prop
        simpa using rel_trans h₁ (rel_mul_right (s : R) hy)
      · simp only [dif_neg hx, dif_neg hy]
        apply ValueGroupWithZero.sound
        · simpa [mul_comm] using h₂
        · simpa [mul_comm] using h₁

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