OAI/GroupTheory/PolycyclicRecognition/Geometry/DiscreteAbelianHeightKernel.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Discrete abelian subgroups of the actual height kernel

The intrinsic kernel realization supplies the unipotence needed by the logarithmic lattice argument. In particular this applies to central subgroups in the remaining nilpotent lattice-finiteness argument.

  1. theorem OAI.PolycyclicRecognition.finitelyGenerated_discrete_abelian_height_kernel line 24