feat(group_theory/nilpotent): p-groups are nilpotent (#11726)

src/data/fintype/basic.lean

@@ -2100,3 +2100,29 @@ begin
   { apply symm,
     exact hf' n m h }
 end
+
+/-- A custom induction principle for fintypes. The base case is a subsingleton type,
+and the induction step is for non-trivial types, and one can assume the hypothesis for
+smaller types (via `fintype.card`).
+
+The major premise is `fintype α`, so to use this with the `induction` tactic you have to give a name
+to that instance and use that name.
+-/
+@[elab_as_eliminator]
+lemma fintype.induction_subsingleton_or_nontrivial
+  {P : Π α [fintype α], Prop} (α : Type*) [fintype α]
+  (hbase : ∀ α [fintype α] [subsingleton α], by exactI P α)
+  (hstep : ∀ α [fintype α] [nontrivial α],
+    by exactI ∀ (ih : ∀ β [fintype β], by exactI ∀ (h : fintype.card β < fintype.card α), P β),
+    P α) :
+  P α :=
+begin
+  obtain ⟨ n, hn ⟩ : ∃ n, fintype.card α = n := ⟨fintype.card α, rfl⟩,
+  unfreezingI { induction n using nat.strong_induction_on with n ih generalizing α },
+  casesI (subsingleton_or_nontrivial α) with hsing hnontriv,
+  { apply hbase, },
+  { apply hstep,
+    introsI β _ hlt,
+    rw hn at hlt,
+    exact (ih (fintype.card β) hlt _ rfl), }
+end

src/group_theory/nilpotent.lean

@@ -7,6 +7,7 @@ Authors: Kevin Buzzard, Ines Wright, Joachim Breitner
 import group_theory.general_commutator
 import group_theory.quotient_group
 import group_theory.solvable
+import group_theory.p_group
 
 /-!
 
@@ -628,7 +629,7 @@ begin
             : nilpotency_class_le_of_ker_le_center _ (le_of_eq (ker_mk _)) _, } }
 end
 
-/-- Quotienting the `center G` reduces the nilpotency class by 1 -/
+/-- The nilpotency class of a non-trivial group is one more than its quotient by the center -/
 lemma nilpotency_class_eq_quotient_center_plus_one [hH : is_nilpotent G] [nontrivial G] :
   group.nilpotency_class G = group.nilpotency_class (G ⧸ center G) + 1 :=
 begin
@@ -640,6 +641,14 @@ begin
   { simp }
 end
 
+/-- If the quotient by `center G` is nilpotent, then so is G. -/
+lemma of_quotient_center_nilpotent (h : is_nilpotent (G ⧸ center G)) : is_nilpotent G :=
+begin
+  obtain ⟨n, hn⟩ := h.nilpotent,
+  use n.succ,
+  simp [← comap_upper_central_series_quotient_center, hn],
+end
+
 end classical
 
 /-- A custom induction principle for nilpotent groups. The base case is a trivial group
@@ -703,3 +712,29 @@ begin
   rw [eq_bot_iff, ←hn],
   exact derived_le_lower_central n,
 end
+
+section classical
+
+open_locale classical -- to get the fintype instance for quotient groups
+
+/-- A p-group is nilpotent -/
+lemma is_p_group.is_nilpotent {G : Type*} [hG : group G] [hf : fintype G]
+  {p : ℕ} (hp : fact (nat.prime p)) (h : is_p_group p G) :
+  is_nilpotent G :=
+begin
+  unfreezingI
+  { revert hG,
+    induction hf using fintype.induction_subsingleton_or_nontrivial with G hG hS G hG hN ih },
+  { apply_instance, },
+  { introI _, intro h,
+    have hc : center G > ⊥ := gt_iff_lt.mp h.bot_lt_center,
+    have hcq : fintype.card (G ⧸ center G) < fintype.card G,
+    { rw card_eq_card_quotient_mul_card_subgroup (center G),
+      apply lt_mul_of_one_lt_right,
+      exact (fintype.card_pos_iff.mpr has_one.nonempty),
+      exact ((subgroup.one_lt_card_iff_ne_bot _).mpr (ne_of_gt hc)), },
+    have hnq : is_nilpotent (G ⧸ center G) := ih _ hcq (h.to_quotient (center G)),
+    exact (of_quotient_center_nilpotent hnq), }
+end
+
+end classical