invertibleOfInvertibleMul — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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