mathlib

076490ae - feat(group_theory/nilpotent): the is_nilpotent_of_finite_tfae theorem (#11835)