no goals
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
⊢ Group.IsNilpotent G
classical
  let ps := (Fintype.card G).factorization.support
  have : ∀ (p : ps) (P : Sylow p G), IsNilpotent (↑P : Subgroup G) := by
    intro p P
    haveI : Fact (Nat.Prime ↑p) := Fact.mk (Nat.prime_of_mem_factorization (Finset.coe_mem p))
    exact P.isPGroup'.isNilpotent
  exact nilpotent_of_mulEquiv e
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
⊢ Group.IsNilpotent G
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
⊢ Group.IsNilpotent G
let ps := (Fintype.card G).factorization.support
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
this : ∀ (p : { x // x ∈ ps }) (P : Sylow (↑p) G), Group.IsNilpotent { x // x ∈ ↑P }
⊢ Group.IsNilpotent G
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
⊢ Group.IsNilpotent G
have : ∀ (p : ps) (P : Sylow p G), IsNilpotent (↑P : Subgroup G) := by
  intro p P
  haveI : Fact (Nat.Prime ↑p) := Fact.mk (Nat.prime_of_mem_factorization (Finset.coe_mem p))
  exact P.isPGroup'.isNilpotent
no goals
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
this : ∀ (p : { x // x ∈ ps }) (P : Sylow (↑p) G), Group.IsNilpotent { x // x ∈ ↑P }
⊢ Group.IsNilpotent G
exact nilpotent_of_mulEquiv e
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
p : { x // x ∈ ps }
P : Sylow (↑p) G
⊢ Group.IsNilpotent { x // x ∈ ↑P }
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
⊢ ∀ (p : { x // x ∈ ps }) (P : Sylow (↑p) G), Group.IsNilpotent { x // x ∈ ↑P }
intro p P
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
p : { x // x ∈ ps }
P : Sylow (↑p) G
this : Fact (Nat.Prime ↑p)
⊢ Group.IsNilpotent { x // x ∈ ↑P }
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
p : { x // x ∈ ps }
P : Sylow (↑p) G
⊢ Group.IsNilpotent { x // x ∈ ↑P }
haveI : Fact (Nat.Prime ↑p) := Fact.mk (Nat.prime_of_mem_factorization (Finset.coe_mem p))
no goals
G : Type u_1
hG : Group G
inst✝ : Fintype G
e : ((p : { x // x ∈ (Nat.factorization (card G)).support }) → (P : Sylow (↑p) G) → { x // x ∈ ↑P }) ≃* G
ps : Finset ℕ := (Nat.factorization (card G)).support
p : { x // x ∈ ps }
P : Sylow (↑p) G
this : Fact (Nat.Prime ↑p)
⊢ Group.IsNilpotent { x // x ∈ ↑P }
exact P.isPGroup'.isNilpotent