mulRight — Mathlib

English

For a fixed invertible b, right multiplication by b induces a bijection between invertible elements: Invertible a ↔ Invertible (a b).

Русский

Для фиксированного обратимого b правое умножение на b задаёт биекцию между обратимыми элементами: Invertible a ⇔ Invertible (a b).

LaTeX

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

Lean4

/-- `invertibleOfMulInvertible` and `invertibleMul` as an equivalence. -/
@[simps apply symm_apply]
def mulRight (a : α) {b : α} (_ : Invertible b) : Invertible a ≃ Invertible (a * b)
    where
  toFun _ := invertibleMul a b
  invFun _ := invertibleOfMulInvertible _ b
  left_inv _ := Subsingleton.elim _ _
  right_inv _ := Subsingleton.elim _ _

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