leftInverse_inv — Mathlib

English

The inverse map has itself as a left inverse; equivalently, Inv.inv is its own left inverse.

Русский

Обратная карта имеет самого себя в качестве левого обратного; то есть Inv.inv является своим собственным левым обратным.

LaTeX

$$$\forall g,\ (Inv.inv)(Inv.inv(g)) = g$$$

Lean4

@[to_additive]
theorem leftInverse_inv : LeftInverse (fun a : G ↦ a⁻¹) fun a ↦ a⁻¹ :=
  inv_inv

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