OAI/GroupTheory/PolycyclicRecognition/Lattices/NilpotentCyclicLatticeExtension.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The cyclic step in nilpotent lattice realization

Given a polynomial lattice model for the kernel and the smooth extension of its conjugation automorphism, nilpotence supplies the real flow and the resulting cyclic extension is a uniform lattice in a constructed solvable Lie group.

  1. theorem OAI.PolycyclicRecognition.nilpotent_cyclic_lattice_extension line 23