OAI/GroupTheory/PolycyclicRecognition/Lattices/SmoothIntegralLatticeRealization.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Realizing a uniform lattice with possibly translated integral fibers

A smooth action of an integral vector group extends after a finite power. Any uniform lattice in the original semidirect group then has a finite-index subgroup which is a uniform lattice in the connected solvable Lie model.

  1. theorem OAI.PolycyclicRecognition.smooth_integral_uniform_lattice_realization line 23