inv_involutive — Mathlib

English

The inverse operation is an involution: applying the inverse twice returns the original element.

Русский

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

LaTeX

$$$\forall g \in G,\ (g^{-1})^{-1} = g$$$

Lean4

@[to_additive (attr := simp)]
theorem inv_involutive : Function.Involutive (Inv.inv : G → G) :=
  inv_inv

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