mulRight_symm — Mathlib

English

For any c ∈ G, the map g ↦ g c is an isometry of G; i.e., edist(g1 c, g2 c) = edist(g1, g2).

Русский

Для любого c ∈ G отображение g ↦ g c является изометрией на G: edist(g1 c, g2 c) = edist(g1, g2).

LaTeX

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

Lean4

@[to_additive (attr := simp)]
theorem mulRight_symm [IsIsometricSMul Gᵐᵒᵖ G] (x : G) : (mulRight x).symm = mulRight x⁻¹ :=
  ext fun _ => rfl

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