English
The map divLeft(a): G ≃ G given by divLeft(a)(b) = a / b is a bijection; its inverse is divLeft(a)^{-1}(b) = b^{-1} a.
Русский
Отображение divLeft(a): G ≃ G, задающее divLeft(a)(b) = a / b, биекция; обратное равно divLeft(a)^{-1}(b) = b^{-1} a.
LaTeX
$$$\\text{divLeft}(a): G \\to G,\\; b \\mapsto a / b \\quad\\text{is a bijection with inverse } b \\mapsto b^{-1} a$$$
Lean4
/-- A version of `Equiv.mulLeft a b⁻¹` that is defeq to `a / b`. -/
@[to_additive (attr := simps) /-- A version of `Equiv.addLeft a (-b)` that is defeq to `a - b`. -/
]
protected def divLeft (a : G) : G ≃ G where
toFun b := a / b
invFun b := b⁻¹ * a
left_inv b := by simp [div_eq_mul_inv]
right_inv b := by simp [div_eq_mul_inv]
