mathlib

1fe9708e - feat(group_theory/nilpotent): is_nilpotent_of_product_of_sylow_group (#11834)