toPerm — Mathlib

English

Given a group α acting on β, each a ∈ α defines a permutation of β given by x ↦ a • x, with inverse a⁻¹ acting as a⁻¹ • x.

Русский

Пусть группа α действует на β; для каждого a ∈ α определена перестановка β по правилу x ↦ a • x, а обратное действие — a⁻¹ • x.

LaTeX

$$$ \text{toPerm}(a) : \mathrm{Equiv.Perm}(β) \quad\text{with}\quad (a\cdot x)^{-1} = a^{-1}\cdot x $$$

Lean4

/-- Given an action of a group `α` on `β`, each `g : α` defines a permutation of `β`. -/
@[to_additive (attr := simps)]
def toPerm (a : α) : Equiv.Perm β :=
  ⟨fun x => a • x, fun x => a⁻¹ • x, inv_smul_smul a, smul_inv_smul a⟩

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