G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Fintype.card G
h : ↑P = ⊥
⊢ p ∣ 1
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Fintype.card G
⊢ ↑P ≠ ⊥
refine' fun h => hp.out.not_dvd_one _
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Fintype.card G
h : ↑P = ⊥
key : p ∣ Fintype.card { x // x ∈ ↑P }
⊢ p ∣ 1
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Fintype.card G
h : ↑P = ⊥
⊢ p ∣ 1
have key : p ∣ card (P : Subgroup G) := P.dvd_card_of_dvd_card hdvd
no goals
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
hdvd : p ∣ Fintype.card G
h : ↑P = ⊥
key : p ∣ Fintype.card { x // x ∈ ↑P }
⊢ p ∣ 1
rwa [h, card_bot] at key