OAI/GroupTheory/PolycyclicRecognition/Lattices/SemidirectUniformLattice.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform lattices in a semidirect product

The lattices in the two factors form a lattice whenever the acting lattice preserves the first lattice. The compact cover uses the inverse action before reducing the first coordinate.

  1. def OAI.PolycyclicRecognition.semidirectLattice line 23
  2. theorem OAI.PolycyclicRecognition.semidirectLattice_discrete line 33
  3. theorem OAI.PolycyclicRecognition.semidirectLattice_uniform line 49