Theorems · Definition · group theory
MulAction.orbit
(γ : Type u_2) → {α : Type u_3} → [SMul γ α] → α → Set αThe orbit of an element under an action.
- Defined in
- Mathlib.GroupTheory.GroupAction.Defs
- Cited by
- 114 results in Mathlib
- Foundations
- Depth 4 from the axioms, rests on 12 definitions · uses no axioms
- Assumes
- SMul
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by128
Results whose statement or proof uses this declaration.
- MulAction.orbitRelproof · cited by 114
- MulAction.orbitRel.Quotient.orbitproof · cited by 15
- Nat.card_zpowersproof · cited by 13
- MulAction.mem_orbitstatement · cited by 10
- MulAction.mem_orbit_selfstatement · cited by 9
- MulAction.mem_orbit_iffstatement · cited by 7
- IsQuotientCoveringMap.apply_eq_iff_mem_orbitstatement · cited by 6
- IsPGroup.card_modEq_card_fixedPointsproof · cited by 4
- MulAction.card_orbit_mul_card_stabilizer_eq_card_groupstatement and proof · cited by 4
- MulAction.IsBlock.ncard_block_mul_ncard_orbit_eqstatement and proof · cited by 4
- MulAction.index_stabilizerstatement and proof · cited by 4
- MulAction.orbitRel.Quotient.orbit_eq_orbit_outstatement and proof · cited by 4