OAI/GroupTheory/PolycyclicRecognition/Lattices/FreeAbelianCyclicLattice.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Realizing nilpotent integral abelian-by-cyclic groups as Lie lattices

The nilpotency class is unrestricted. The real action is constructed by the finite logarithm of the extended integral automorphism.

  1. def OAI.PolycyclicRecognition.realIntegralGroupAut line 18
  2. theorem OAI.PolycyclicRecognition.contMDiff_realIntegralGroupAut line 23
  3. theorem OAI.PolycyclicRecognition.realIntegralGroupAut_lattice line 27
  4. theorem OAI.PolycyclicRecognition.freeAbelian_cyclic_nilpotent_lattice line 34