G : Type u
α : Type v
β : Type w
inst✝² : Group G
inst✝¹ : Fintype G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ 1 ∣ Fintype.card G
⊢ p ∣ Fintype.card { x // x ∈ ↑P }
G : Type u
α : Type v
β : Type w
inst✝² : Group G
inst✝¹ : Fintype G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Fintype.card G
⊢ p ∣ Fintype.card { x // x ∈ ↑P }
rw [← pow_one p] at hdvd
G : Type u
α : Type v
β : Type w
inst✝² : Group G
inst✝¹ : Fintype G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ 1 ∣ Fintype.card G
key : p ^ 1 ∣ Fintype.card { x // x ∈ ↑P }
⊢ p ∣ Fintype.card { x // x ∈ ↑P }
G : Type u
α : Type v
β : Type w
inst✝² : Group G
inst✝¹ : Fintype G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ 1 ∣ Fintype.card G
⊢ p ∣ Fintype.card { x // x ∈ ↑P }
have key := P.pow_dvd_card_of_pow_dvd_card hdvd
no goals
G : Type u
α : Type v
β : Type w
inst✝² : Group G
inst✝¹ : Fintype G
p : ℕ
inst✝ : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ^ 1 ∣ Fintype.card G
key : p ^ 1 ∣ Fintype.card { x // x ∈ ↑P }
⊢ p ∣ Fintype.card { x // x ∈ ↑P }
rwa [pow_one] at key