feat(group_theory/nilpotent): Add equality theorems for nilpotency class (#11540)
the nilpotency class can be defined as the length of the
upper central series, the lower central series, or as the shortest
length across all ascending or descending series.
In order to use the equivalence proofs between the various definition
of nilpotency in these lemmas, I had to reorder them to put the `∃n` in
front.
mathlib
b87449ab - feat(group_theory/nilpotent): Add equality theorems for nilpotency class (#11540)
