inverse_add_inverse — Mathlib

English

For a and b invertible in a semiring, ⅟a + ⅟b = ⅟a * (a + b) * ⅟b.

Русский

Для обратимых a,b в полупрямой системе: ⅟a + ⅟b = ⅟a • (a + b) • ⅟b.

LaTeX

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

Lean4

/-- A version of `inv_add_inv'` for `Ring.inverse`. -/
theorem inverse_add_inverse [Semiring R] {a b : R} (h : IsUnit a ↔ IsUnit b) :
    Ring.inverse a + Ring.inverse b = Ring.inverse a * (a + b) * 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_add_invOf]
  · have hb := h.not.mp ha
    simp [inverse_non_unit, ha, hb]

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