English
There is a canonical equivalence on a group G, called divRight, given by x ↦ x/a; its inverse is x ↦ x·a. Equivalently, the right-division by a defines a bijection with inverse right-multiplication by a.
Русский
Существует каноническая эквивалентность на группе G, называемая divRight, заданная отображением x ↦ x/a; обратное ей — x ↦ x·a. Эквивалентность задаёт биективность деления справа на a с обратной операцией — умножением справа на a.
LaTeX
$$$\\mathrm{divRight}(a) : G \\to G,\\quad \\mathrm{divRight}(a)(x)=\\dfrac{x}{a}=x\\cdot a^{-1}$$$
Lean4
/-- A version of `Equiv.mulRight a⁻¹ b` that is defeq to `b / a`. -/
@[to_additive (attr := simps) /-- A version of `Equiv.addRight (-a) b` that is defeq to `b - a`. -/
]
protected def divRight (a : G) : G ≃ G where
toFun b := b / a
invFun b := b * a
left_inv b := by simp [div_eq_mul_inv]
right_inv b := by simp [div_eq_mul_inv]
