OAI/GroupTheory/PolycyclicRecognition/Lattices/AbelianCyclicLattice.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Lattice realization for torsion-free nilpotent groups with abelian cyclic kernel

The nilpotency class is unrestricted. An abstract abelian kernel is identified with its integral basis before applying the constructed real flow.

  1. theorem OAI.PolycyclicRecognition.abelian_cyclic_nilpotent_lattice line 17
  2. theorem OAI.PolycyclicRecognition.nilpotent_abelian_kernel_cyclic_lattice line 39