case intro
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Fintype.card { x // x ∈ ↑P } = p ^ n
⊢ Fintype.card { x // x ∈ ↑P } = p ^ ↑(Nat.factorization (Fintype.card G)) p
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
⊢ Fintype.card { x // x ∈ ↑P } = p ^ ↑(Nat.factorization (Fintype.card G)) p
obtain ⟨n, heq : card P = _⟩ := IsPGroup.iff_card.mp P.isPGroup'
case intro
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Fintype.card { x // x ∈ ↑P } = p ^ n
⊢ Fintype.card { x // x ∈ ↑P } ∣ p ^ ↑(Nat.factorization (Fintype.card G)) p
case intro
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Fintype.card { x // x ∈ ↑P } = p ^ n
⊢ Fintype.card { x // x ∈ ↑P } = p ^ ↑(Nat.factorization (Fintype.card G)) p
refine' Nat.dvd_antisymm _ (P.pow_dvd_card_of_pow_dvd_card (Nat.ord_proj_dvd _ p))
case intro
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Fintype.card { x // x ∈ ↑P } = p ^ n
⊢ Fintype.card { x // x ∈ ↑P } ∣ Fintype.card G
case intro
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Fintype.card { x // x ∈ ↑P } = p ^ n
⊢ Fintype.card { x // x ∈ ↑P } ∣ p ^ ↑(Nat.factorization (Fintype.card G)) p
rw [heq, ← hp.out.pow_dvd_iff_dvd_ord_proj (show card G ≠ 0 from card_ne_zero), ← heq]
no goals
case intro
G : Type u
α : Type v
β : Type w
inst✝¹ : Group G
inst✝ : Fintype G
p : ℕ
hp : Fact (Nat.Prime p)
P : Sylow p G
n : ℕ
heq : Fintype.card { x // x ∈ ↑P } = p ^ n
⊢ Fintype.card { x // x ∈ ↑P } ∣ Fintype.card G
exact P.1.card_subgroup_dvd_card