OAI/GroupTheory/PolycyclicRecognition/Finiteness/NilpotentLatticeFiniteness.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Finiteness of a nilpotent kernel below a lattice quotient

The rational top class supplies the lower dimension bound. Integral orientation homology and exhaustion stabilization then force finite generation.

  1. theorem OAI.PolycyclicRecognition.nilpotent_kernel_finitelyGenerated_of_latticeQuotient line 18
  2. theorem OAI.PolycyclicRecognition.polycyclic_of_nilpotent_latticeQuotient line 48