inv — Mathlib

English

Inversion on a group-like structure yields an involutive permutation on the underlying set.

Русский

Обратное к группе-подобной структуре образует взаимно однозначную перестановку множества.

LaTeX

$$$\text{Equiv.inv}(G) : G \to G$ is an involutive permutation, i.e., (\text{Equiv.inv}(G))^{2} = id$.$$

Lean4

/-- Inversion on a `Group` or `GroupWithZero` is a permutation of the underlying type. -/
@[to_additive (attr := simps! -fullyApplied apply) /--
    Negation on an `AddGroup` is a permutation of the underlying type. -/
    ]
protected def inv : Perm G :=
  inv_involutive.toPerm _

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