inv_comp_inv — Mathlib

English

The inverse operation composed with itself is the identity; applying inverse twice yields the original element.

Русский

Обратная операция в композиции с самой собой дает тождественную; применение обратного дважды возвращает исходное.

LaTeX

$$$\forall g \in G,\ (Inv.inv \circ Inv.inv)(g) = g$$$

Lean4

@[to_additive]
theorem inv_comp_inv : Inv.inv ∘ Inv.inv = @id G :=
  inv_involutive.comp_self

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