OAI/GroupTheory/PolycyclicRecognition/Algebra/MaximalNilpotentNormal.lean

The centralizer of a maximal nilpotent normal subgroup

In a solvable group, a maximal nilpotent normal subgroup contains its own centralizer. Descend the derived series of that centralizer: if the next term lies in the maximal subgroup, the current term has class at most two and centralizes it, so their product contradicts maximality unless it was already contained. Finite integral cohomological dimension supplies the maximal subgroup by the uniform nilpotence bound.