invOf_mul_self' — Mathlib

English

There are bijections between invertible elements given left or right multiplication by a fixed invertible element.

Русский

Существуют биекции между обратимыми элементами, получаемые при левом или правом умножении на заданный обратимый элемент.

LaTeX

$$$\text{Invertible}(a) \cong \text{Invertible}(a b) \quad\text{and}\quad \text{Invertible}(b) \cong \text{Invertible}(a b)$$$

Lean4

@[simp]
theorem invOf_mul_self' [Mul α] [One α] (a : α) {_ : Invertible a} : ⅟a * a = 1 :=
  Invertible.invOf_mul_self

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