Nilpotent.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The nilpotent conclusion in recognition

Finitely generated nilpotent groups are polycyclic. Consequently a finitely generated virtually nilpotent group is virtually polycyclic, by finite generation of the finite-index nilpotent subgroup.

theorem OAI.PolycyclicRecognition.isPolycyclic_of_finitelyGenerated_nilpotent line 20
Source documentation
Finite generation and nilpotence yield an actual finite cyclic subnormal series.
```
theorem isPolycyclic_of_finitelyGenerated_nilpotent [Group.IsNilpotent G] :
    IsPolycyclic G := by
…
```
Mentions: OAI.PolycyclicRecognition.IsPolycyclic
theorem OAI.PolycyclicRecognition.isVirtuallyPolycyclic_of_finitelyGenerated_virtuallyNilpotent line 26
Source documentation
Schreier finite generation applies to the nilpotent finite-index subgroup.
```
theorem isVirtuallyPolycyclic_of_finitelyGenerated_virtuallyNilpotent
    (hG : Group.IsVirtuallyNilpotent G) : IsVirtuallyPolycyclic G := by
…
```