inverse_sub_inverse — Mathlib

English

For a ring R and a,b with IsUnit, IsUnit b, the identity inv(a) - inv(b) = inv(a) * (b - a) * inv(b) holds.

Русский

Для кольца R и обратимых a,b имеет место inv(a) − inv(b) = inv(a) (b − a) inv(b).

LaTeX

$$⅟a - ⅟b = ⅟a * (b - a) * ⅟b$$

Lean4

/-- A version of `inv_sub_inv'` for `Ring.inverse`. -/
theorem inverse_sub_inverse [Ring R] {a b : R} (h : IsUnit a ↔ IsUnit b) :
    Ring.inverse a - Ring.inverse b = Ring.inverse a * (b - a) * Ring.inverse b :=
  by
  by_cases ha : IsUnit a
  · have hb := h.mp ha
    obtain ⟨ia⟩ := ha.nonempty_invertible
    obtain ⟨ib⟩ := hb.nonempty_invertible
    simp_rw [inverse_invertible, invOf_sub_invOf]
  · have hb := h.not.mp ha
    simp [inverse_non_unit, ha, hb]

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