mathlib3

f7a597ad - feat(group_theory/nilpotent): add nilpotency_class inequalities (#11585)

feat(group_theory/nilpotent): add nilpotency_class inequalities (#11585) Every theorem that proves `nilpotency G'` (e.g. for subgroups, images, preimages) should be accompanied by a lemma relating their `nilpotency_class`, so add thse lmmeas for subgroups and preimages. Also add nilpotency lemmas for surjective homomorphisms and quotions, including nilpotency_class lemmas.