mul_inv_cancel — Mathlib

English

In a localization by nonzero divisors, every nonzero element has a two-sided inverse: x · x^{-1} = 1 for x ≠ 0.

Русский

В локализации по нулевым делителям у каждого ненулевого элемента есть двусторонний обратный: x · x^{-1} = 1 при x ≠ 0.

LaTeX

$$∀ x ≠ 0, x · x^{-1} = 1 in OreLocalization(nonZeroDivisors(R)) R$$

Lean4

protected theorem mul_inv_cancel (x : R[R⁰⁻¹]) (h : x ≠ 0) : x * x⁻¹ = 1 :=
  by
  induction x with
  | _ r s
  rw [OreLocalization.inv_def, OreLocalization.one_def]
  have hr : r ≠ 0 := by
    rintro rfl
    simp at h
  simp only [hr]
  with_unfolding_all apply OreLocalization.mul_inv ⟨r, _⟩

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