inv — Mathlib

Lean4
/-- The inversion of Ore fractions for a ring without zero divisors, satisfying `0⁻¹ = 0` and
`(r /ₒ r')⁻¹ = r' /ₒ r` for `r ≠ 0`. -/
@[irreducible]
protected noncomputable def inv : R[R⁰⁻¹] → R[R⁰⁻¹] :=
  liftExpand (fun r s => if hr : r = (0 : R) then (0 : R[R⁰⁻¹]) else s /ₒ ⟨r, mem_nonZeroDivisors_of_ne_zero hr⟩)
    (by
      intro r t s hst
      by_cases hr : r = 0
      · simp [hr]
      · by_cases ht : t = 0
        · exfalso
          apply nonZeroDivisors.coe_ne_zero ⟨_, hst⟩
          simp [ht]
        · simp only [hr, ht, dif_neg, not_false_iff, or_self_iff, mul_eq_zero, smul_eq_mul]
          apply OreLocalization.expand)
Похожие утверждения