Theorems · Definition · group theory

MulAction.toPermHom

(G : Type u_1) → (α : Type u_5) → [inst : Group G] → [MulAction G α] → G →* Equiv.Perm α

Given an action of a group G on a set α, each g : G defines a permutation of α.

Defined in

Mathlib.Algebra.Group.Action.End

Cited by

16 results in Mathlib

Foundations

Depth 22 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupMulAction