invertibleMul — Mathlib

English

The inverse of a product is the product of inverses in reverse order: (a*b)^{-1} = b^{-1} a^{-1}.

Русский

Обратное произведения — это обратные отдельных элементов в обратном порядке: (a*b)^{-1} = b^{-1} a^{-1}.

LaTeX

$$$ (a b)^{-1} = b^{-1} a^{-1} $$$

Lean4

/-- `⅟b * ⅟a` is the inverse of `a * b` -/
def invertibleMul [Monoid α] (a b : α) [Invertible a] [Invertible b] : Invertible (a * b) :=
  ⟨⅟b * ⅟a, by simp [← mul_assoc], by simp [← mul_assoc]⟩

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