Theorems · Theorem · group theory

Group.nilpotent_center_quotient_ind

∀ {P : (G : Type u_2) → [inst : Group G] → [Group.IsNilpotent G] → Prop} (G : Type u_2) [inst : Group G]
  [inst_1 : Group.IsNilpotent G],
  (∀ (G : Type u_2) [inst : Group G] [inst_2 : Subsingleton G], P G) →
    (∀ (G : Type u_2) [inst : Group G] [inst_2 : Group.IsNilpotent G], P (G ⧸ Subgroup.center G) → P G) → P G

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.

Defined in

Mathlib.GroupTheory.Nilpotent

Cited by

2 results in Mathlib

Foundations

Depth 100 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupGroup.IsNilpotent