OAI/GroupTheory/PolycyclicRecognition/Algebra/DiscreteUnipotentAbelian.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Discrete abelian unipotent groups are finitely generated

The logarithm is additive on a commuting unipotent group. The inducing representation and the continuous exponential make its logarithmic image a discrete integral submodule of a finite-dimensional real vector space. This is the abelian and central-subgroup step of lattice finiteness.

  1. theorem OAI.PolycyclicRecognition.finitelyGenerated_of_discrete_unipotent_representation line 25
  2. theorem OAI.PolycyclicRecognition.polycyclic_of_discrete_unipotent_representation line 85