Finite nilpotent groups characterisations

[nomeata]

I’ll use this issue to track the progress of my current idle project of formalizing the various equivalent definitions for nilpotent finite group, which was suggested to me by @kbuzzard. This is mostly for myself to keep an overview of things, and maybe the bragging rights afterwards, but of course comments are welcome.

For a finite group, the following are equivalent (see e.g. on groupprops):

1. It is a nilpotent group.
2. It satisfies the normalizer condition i.e. it has no proper self-normalizing subgroup.
3. Every maximal subgroup is normal.
4. All its Sylow subgroups are normal.
5. It is the direct product of its Sylow subgroups.

I’ll proceed according to the following plan (per bullet PRs are topologically sorted)

• 1 → 2:
  • [Merged by Bors] - feat(group_theory.nilpotent): add *_central_series_one G 1 = … simp lemmas #11584
  • [Merged by Bors] - feat(group_theory/nilpotent): add nilpotency_class inequalities #11585
  • [Merged by Bors] - feat(group_theory/subgroup/basic): add normalizer_condition definition #11587
  • [Merged by Bors] - feat(group_theory/subgroup/basic): add center_le_normalizer #11590
  • [Merged by Bors] - feat(data/quot): add subsingleton instances #11668
  • [Merged by Bors] - feat(group_theory/nilpotent): add upper_central_series_eq_top_iff_nilpotency_class_le #11670
  • [Merged by Bors] - feat(group_theory/nilpotent): add lemmas about G / center G #11592
  • [Merged by Bors] - feat(group_theory/nilpotent): add nilpotent implies normalizer condition #11586
• 2 → 3:
  • [Merged by Bors] - feat(group_theory/subgroup/basic): normalizer condition implies max subgroups normal #11597
• 3 → 4:
  • [Merged by Bors] - feat(group_theory/subgroup/basic): add lemmas related to map, comap, normalizer #11637
  • [Merged by Bors] - feat(group_theory/sylow): preimages of sylow groups #11722
  • [Merged by Bors] - feat(order/atoms): finite orders are (co)atomic #11930
  • [Merged by Bors] - feat(group_theory/sylow): all max groups normal imply sylow normal #11841
• 4 → 5:
  • [Merged by Bors] - feat(group_theory/subgroup/basic): add commute_of_normal_of_disjoint #11751
  • [Merged by Bors] - feat(group_theory/p_group): p-groups with different p are disjoint #11752
  • [Merged by Bors] - feat(group_theory/p_group): finite p-groups with different p have coprime orders #11775
  • [Merged by Bors] - feat(group_theory/sylow): the cardinality of a sylow group #11776
  • [Merged by Bors] - feat(data/nat/gcd): add coprime_prod_left and coprime_prod_right #12268
  • [Merged by Bors] - feat(algebra/group/to_additive): let to_additive turn pow into nsmul #12477
  • [Merged by Bors] - feat(data/list/prod_monoid): add prod_eq_pow_card #12473
  • [Merged by Bors] - fix(algebra/group/pi): Fix apply-simp-lemmas for monoid_hom.single #12474
  • [Merged by Bors] - feat(data/finset/noncomm_prod): finite pi lemmas #12291
  • [Merged by Bors] - feat(group_theory/subgroup/basic): disjoint_iff_mul_eq_one #12505
  • [Merged by Bors] - feat(data/finset/noncomm_prod): add noncomm_prod_commute #12521
  • [Merged by Bors] - feat(group_theory/subgroup/basic): {multiset_,}noncomm_prod_mem #12523
  • [Merged by Bors] - feat(data/finset/noncomm_prod): add noncomm_prod_mul_distrib #12524
  • [Merged by Bors] - feat(group_theory/subgroup/basic): add eq_one_of_noncomm_prod_eq_one_of_independent #12525
  • [Merged by Bors] - feat(group_theory/noncomm_pi_coprod): homomorphism from pi monoids or groups #11744
  • [Merged by Bors] - feat(data/equiv/{basic,mul_equiv)}: add Pi_subsingleton #12040
  • [Merged by Bors] - feat(group_theory/sylow): direct product of sylow groups if all normal #11778
• 5 → 1:
  • [Merged by Bors] - feat(group_theory/nilpotent): p-groups are nilpotent #11726
  • [Merged by Bors] - feat(group_theory/subgroup/basic): add pi subgroups #11801
  • [Merged by Bors] - feat(data/pi): provide pi.mul_single #11849
  • [Merged by Bors] - feat(group_theory/general_commutator): subgroup.pi commutes with the general_commutator #11825
  • [Merged by Bors] - feat(group_theory/nilpotent): n-ary products of nilpotent group #11829
  • [Merged by Bors] - feat(group_theory/nilpotent): is_nilpotent_of_product_of_sylow_group #11834
• [Merged by Bors] - feat(group_theory/nilpotent): the is_nilpotent_of_finite_tfae theorem #11835

Opportunistic PRs or PRs that weren’t used in the end:

• [Merged by Bors] - feat(group_theory/nilpotent): abelian iff nilpotency class ≤ 1 #11718
• [Merged by Bors] - feat(group_theory/sylow): add characteristic_of_normal #11636
• [Merged by Bors] - feat(group_theory/subgroup/basic): add commute_of_normal_of_disjoint #11751
• [Merged by Bors] - feat(group_theory/submonoid/operations): prod_le_iff and le_prod_iff, also for groups and modules #11898
• [Merged by Bors] - feat(group_theory/general_commutator): subgroup.prod commutes with the general_commutator #11818
• [Merged by Bors] - feat(group_theory/nilpotent): products of nilpotent groups #11827
• [Merged by Bors] - feat(group_theory/sylow): the normalizer is self-normalizing #11638
• [Merged by Bors] - feat(data/finset/noncomm_prod): add noncomm_prod_congr #12520

[nomeata]

With 076490a 5 this saga comes to an end merge.