mathlib

1373d548 - feat(group_theory/nilpotent): add nilpotent implies normalizer condition (#11586)