divLeft — Mathlib

English

For any fixed c ∈ G, the map y ↦ c / y is an isometry of G; i.e., edist(c/y1, c/y2) = edist(y1, y2) for all y1,y2 ∈ G.

Русский

Для фиксированного c ∈ G отображение y ↦ c / y является изометрией на G; т.е. edist(c/y1, c/y2) = edist(y1, y2) для всех y1,y2.

LaTeX

$$$\mathrm{edist}(\tfrac{c}{y_1}, \tfrac{c}{y_2}) = \mathrm{edist}(y_1, y_2)$$$

Lean4

/-- Division `y ↦ x / y` as an `IsometryEquiv`. -/
@[to_additive (attr := simps! apply symm_apply toEquiv) /-- Subtraction `y ↦ x - y` as an `IsometryEquiv`. -/
    ]
def divLeft (c : G) : G ≃ᵢ G where
  toEquiv := Equiv.divLeft c
  isometry_toFun := edist_div_left c

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