invertibleOfMulInvertible — Mathlib

English

If a b is invertible and b is invertible, then a is invertible; its inverse is b (a b)^{-1}.

Русский

Если a b обратимо и b обратимо, то a обратимо; обратное к a есть b (a b)^{-1}.

LaTeX

$$$\text{Invertible}(a) \land \text{Invertible}(b) \implies \text{Invertible}(a b) \text{ with } \operatorname{inv}(a) = b \cdot (a b)^{-1}$$$

Lean4

/-- This is the `Invertible` version of `Units.isUnit_mul_units` -/
abbrev invertibleOfMulInvertible (a b : α) [Invertible (a * b)] [Invertible b] : Invertible a
    where
  invOf := b * ⅟(a * b)
  invOf_mul_self := by
    rw [← (isUnit_of_invertible b).mul_left_inj, mul_assoc, mul_assoc, invOf_mul_self, mul_one, one_mul]
  mul_invOf_self := by rw [← mul_assoc, mul_invOf_self]

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