inv_add_inv' — Mathlib

English

For nonzero a,b with a,b commuting, a^{-1} + b^{-1} = (a+b)/(ab).

Русский

Для взаимно коммутирующихся ненулевых a,b: a^{-1} + b^{-1} = (a+b)/(ab).

LaTeX

$$$$a^{-1} + b^{-1} = \frac{a+b}{ab} \quad (a,b\neq 0,\; ab=ba).$$$$

Lean4

/-- See `inv_add_inv` for the more convenient version when `K` is commutative. -/
theorem inv_add_inv' (ha : a ≠ 0) (hb : b ≠ 0) : a⁻¹ + b⁻¹ = a⁻¹ * (a + b) * b⁻¹ :=
  let _ := invertibleOfNonzero ha;
  let _ := invertibleOfNonzero hb;
  invOf_add_invOf a b

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