English
For any c ∈ G, the map y ↦ y / c is an isometry of G; equivalently, edist(a/c, b/c) = edist(a,b) for all a,b ∈ G.
Русский
Для любого c ∈ G отображение y ↦ y / c является изометрией на G; то есть edist(a/c, b/c) = edist(a,b) для всех a,b ∈ G.
LaTeX
$$$\mathrm{edist}(a/c, b/c) = \mathrm{edist}(a,b)$$$
Lean4
/-- Division `y ↦ y / x` as an `IsometryEquiv`. -/
@[to_additive (attr := simps! apply toEquiv) /-- Subtraction `y ↦ y - x` as an `IsometryEquiv`. -/
]
def divRight [IsIsometricSMul Gᵐᵒᵖ G] (c : G) : G ≃ᵢ G
where
toEquiv := Equiv.divRight c
isometry_toFun a b := edist_div_right a b c