p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
⊢ ∃ n, card ↑(orbit G a) = p ^ n
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
⊢ ∃ n, card ↑(orbit G a) = p ^ n
let ϕ := orbitEquivQuotientStabilizer G a
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this : Fintype (G ⧸ stabilizer G a)
⊢ ∃ n, card ↑(orbit G a) = p ^ n
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
⊢ ∃ n, card ↑(orbit G a) = p ^ n
haveI := Fintype.ofEquiv (orbit G a) ϕ
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Fintype (G ⧸ stabilizer G a)
this : Subgroup.FiniteIndex (stabilizer G a)
⊢ ∃ n, card ↑(orbit G a) = p ^ n
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this : Fintype (G ⧸ stabilizer G a)
⊢ ∃ n, card ↑(orbit G a) = p ^ n
haveI := (stabilizer G a).finiteIndex_of_finite_quotient
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Fintype (G ⧸ stabilizer G a)
this : Subgroup.FiniteIndex (stabilizer G a)
⊢ ∃ n, Subgroup.index (stabilizer G a) = p ^ n
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Fintype (G ⧸ stabilizer G a)
this : Subgroup.FiniteIndex (stabilizer G a)
⊢ ∃ n, card ↑(orbit G a) = p ^ n
rw [card_congr ϕ, ← Subgroup.index_eq_card]
no goals
p : ℕ
G : Type u_2
inst✝² : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
α : Type u_1
inst✝¹ : MulAction G α
a : α
inst✝ : Fintype ↑(orbit G a)
ϕ : ↑(orbit G a) ≃ G ⧸ stabilizer G a := orbitEquivQuotientStabilizer G a
this✝ : Fintype (G ⧸ stabilizer G a)
this : Subgroup.FiniteIndex (stabilizer G a)
⊢ ∃ n, Subgroup.index (stabilizer G a) = p ^ n
exact hG.index (stabilizer G a)