Theorems · Definition · group theory
MulAction.toPerm
{α : Type u_5} → {β : Type u_6} → [inst : Group α] → [MulAction α β] → α → Equiv.Perm βGiven an action of a group α on β, each g : α defines a permutation of β.
- Defined in
- Mathlib.Algebra.Group.Action.Basic
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses propext
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Groupstatement and proof · cited by 6,238
- Equiv.Permstatement · cited by 1,375
- MulActionstatement and proof · cited by 1,294
- inv_smul_smulproof · cited by 76
- smul_inv_smulproof · cited by 53
Cited by35
Results whose statement or proof uses this declaration.
- Homeomorph.smulproof · cited by 21
- Set.mem_smul_set_iff_inv_smul_memproof · cited by 18
- MulAction.toPermHomproof · cited by 16
- Set.preimage_smulproof · cited by 15
- Set.subset_smul_set_iffproof · cited by 13
- MulAction.toPerm_applystatement and proof · cited by 12
- MulAction.bijectiveproof · cited by 11
- Set.smul_set_subset_iff_subset_inv_smul_setproof · cited by 9
- IsometryEquiv.constSMulproof · cited by 8
- MeasurableEquiv.smulproof · cited by 7
- MulAction.toPermHom_applystatement · cited by 7
- Diffeomorph.smulproof · cited by 4