def GroupActions.stabilizerSet {α : Type u_2} (G : Type u_3) [Group G] [MulAction G α] (s : α) : Set G

theorem GroupActions.card_eq_sum_orbit_sizes (G : Type u_3) (α : Type u_4) [Group G] [MulAction G α] [Fintype α] [Fintype (MulAction.orbitRel.Quotient G α)] [(ω : MulAction.orbitRel.Quotient G α) → Fintype ↑ω.orbit] : Fintype.card α = ∑ ω : MulAction.orbitRel.Quotient G α, Fintype.card ↑ω.orbit

noncomputable def GroupActions.orbitEquivQuotientStabilizer (G : Type u_3) {α : Type u_4} [Group G] [MulAction G α] (s : α) : ↑(MulAction.orbit G s) ≃ G ⧸ MulAction.stabilizer G s

theorem GroupActions.card_orbit_eq_index_stabilizer (G : Type u_3) {α : Type u_4} [Group G] [MulAction G α] (s : α) : (MulAction.stabilizer G s).index = (MulAction.orbit G s).ncard