OAI/GroupTheory/PolycyclicRecognition/Lattices/AbelianLatticeRealization.lean
2 declarations, 0 contain sorry, 0 declared as axioms
Solvable lattice realization for virtually abelian groups
The finite-index torsion-free subgroup is an integral lattice. Its embedding into the actual additive vector Lie group has a compact fundamental cover. This discharges the virtually abelian case of Dekimpe's realization input.
- theorem
OAI.PolycyclicRecognition.solvable_lattice_realization_of_finiteIndex_abelianline 18 - theorem
OAI.PolycyclicRecognition.dekimpe_realization_of_finiteIndex_abelianline 37