English
There is a custom induction principle for nilpotent groups: if a proposition P holds for trivial groups and is preserved when passing to G/Z(G) from G, then P holds for all nilpotent groups.
Русский
Существует индивидуальная метод индукции по нильпотентным группам: если свойство P верно для тривиальных групп и сохраняется при переходе к G/Z(G) от G, то P верно для всех нильпотентных групп.
LaTeX
$$@[elab_as_elim] (P) (G) [IsNilpotent G] → (∀ G [Subsingleton G], P G) → (∀ G [IsNilpotent G], P (G/Z(G)) → P G) → P G$$
Lean4
/-- A custom induction principle for nilpotent groups. The base case is a trivial group
(`subsingleton G`), and in the induction step, one can assume the hypothesis for
the group quotiented by its center. -/
@[elab_as_elim]
theorem nilpotent_center_quotient_ind {P : ∀ (G) [Group G] [IsNilpotent G], Prop} (G : Type*) [Group G] [IsNilpotent G]
(hbase : ∀ (G) [Group G] [Subsingleton G], P G) (hstep : ∀ (G) [Group G] [IsNilpotent G], P (G ⧸ center G) → P G) :
P G := by
obtain ⟨n, h⟩ : ∃ n, Group.nilpotencyClass G = n := ⟨_, rfl⟩
induction n generalizing G with
| zero =>
haveI := nilpotencyClass_zero_iff_subsingleton.mp h
exact hbase _
| succ n
ih =>
have hn : Group.nilpotencyClass (G ⧸ center G) = n := by simp [nilpotencyClass_quotient_center, h]
exact hstep _ (ih _ hn)
