OAI/GroupTheory/PolycyclicRecognition/Geometry/HeightKernelNilpotentStructure.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Locally nilpotent height kernels

The coefficient dimension and finite-subgroup order bound imply torsion freeness and finite rank of the kernel.

  1. theorem OAI.PolycyclicRecognition.TypeFPInfinity.heightKernel_locallyNilpotent_nilpotent line 18
  2. theorem OAI.PolycyclicRecognition.TypeFPInfinity.heightKernel_locallyNilpotent_structure line 37
  3. theorem OAI.PolycyclicRecognition.TypeFPInfinity.heightKernel_locallyNilpotent_virtualSolvable line 60