isometry_inv — Mathlib

English

The inversion map on a group G is an isometry with respect to the induced isometric SMul structure.

Русский

Обратная карта в группе G является изометрией относительно индуцированной изометрической SMul-структуры.

LaTeX

$$$\text{Isometry }(\mathrm{Inv}.inv: G \to G)$$$

Lean4

@[to_additive]
theorem isometry_inv [PseudoEMetricSpace G] [IsIsometricSMul G G] [IsIsometricSMul Gᵐᵒᵖ G] :
    Isometry (Inv.inv : G → G) :=
  edist_inv_inv

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