mathlib
d6440a84 - feat(group_theory/nilpotent): add lemmas about `G / center G` (#11592)

Commit
3 years ago
feat(group_theory/nilpotent): add lemmas about `G / center G` (#11592) in particular its nilpotency class and an induction principle based on that.
Author
Parents
Loading