mulLeft — Mathlib

English

For each fixed c ∈ G, the map y ↦ c • y is an isometry of G (with the group metric), 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 ∈ G.

LaTeX

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

Lean4

/-- Multiplication `y ↦ x * y` as an `IsometryEquiv`. -/
@[to_additive (attr := simps! apply toEquiv) /-- Addition `y ↦ x + y` as an `IsometryEquiv`. -/
    ]
def mulLeft [IsIsometricSMul G G] (c : G) : G ≃ᵢ G
    where
  toEquiv := Equiv.mulLeft c
  isometry_toFun := edist_mul_left c

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