English
For a fixed invertible a, left multiplication by a induces a bijection between invertible elements: Invertible b ↔ Invertible (a b).
Русский
Для фиксированного обратимого a левостороннее умножение на a задаёт биекцию между обратимыми элементами: Invertible b ⇔ Invertible (a b).
LaTeX
$$$\text{Invertible}(b) \cong \text{Invertible}(a b)$$$
Lean4
/-- `invertibleOfInvertibleMul` and `invertibleMul` as an equivalence. -/
@[simps apply symm_apply]
def mulLeft {a : α} (_ : Invertible a) (b : α) : Invertible b ≃ Invertible (a * b)
where
toFun _ := invertibleMul a b
invFun _ := invertibleOfInvertibleMul a _
left_inv _ := Subsingleton.elim _ _
right_inv _ := Subsingleton.elim _ _
