Theorems · Theorem · group theory

AddGroup.nilpotent_center_quotient_ind

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

A custom induction principle for nilpotent additive groups. The base case is a trivial group (subsingleton G), and in the induction step, one can assume the hypothesis for the additive group quotiented by its center.

Defined in

Mathlib.GroupTheory.Nilpotent

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroup.IsNilpotent