mulRight — Mathlib

English

For any c ∈ G, the map g ↦ c g is an isometry of G (same as 206694).

Русский

Для любого c ∈ G отображение g ↦ c g является изометрией на G.

LaTeX

$$$\mathrm{edist}(c\cdot g_1, c\cdot g_2) = \mathrm{edist}(g_1, g_2)$$$

Lean4

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

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