Theorems · Definition · group theory
AddAction.toPerm
{α : Type u_5} → {β : Type u_6} → [inst : AddGroup α] → [AddAction α β] → α → Equiv.Perm βGiven an action of an additive group α on β, each g : α defines a permutation of β.
- Defined in
- Mathlib.Algebra.Group.Action.Basic
- Cited by
- 21 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.
Cites6
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- AddGroupstatement and proof · cited by 4,410
- HVAdd.hVAddproof · cited by 1,820
- Equiv.Permstatement · cited by 1,375
- AddActionstatement and proof · cited by 820
- neg_vadd_vaddproof · cited by 34
- vadd_neg_vaddproof · cited by 31
Cited by25
Results whose statement or proof uses this declaration.
- Set.mem_vadd_set_iff_neg_vadd_memproof · cited by 24
- Homeomorph.vaddproof · cited by 14
- Set.preimage_vaddproof · cited by 14
- IsometryEquiv.constVAddproof · cited by 8
- AddAction.bijectiveproof · cited by 6
- AddAction.mem_stabilizer_setproof · cited by 5
- MeasurableEquiv.vaddproof · cited by 5
- Diffeomorph.vaddproof · cited by 4
- AddAction.toPerm_applystatement and proof · cited by 4
- Set.subset_vadd_set_iffproof · cited by 3
- ProperVAdd.isCompact_setOfPred_inter_nonemptyproof · cited by 2
- AddAction.toPerm_symm_applystatement and proof · cited by 2