OAI/GroupTheory/PolycyclicRecognition/Lattices/BilinearCentralLattice.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform lattices for integral bilinear central extensions

The central coordinate of a fundamental-domain representative is reduced after subtracting the bilinear correction from the first coordinate.

  1. def OAI.PolycyclicRecognition.bilinearCentralLattice line 22
  2. theorem OAI.PolycyclicRecognition.bilinearCentralLattice_discrete line 35
  3. theorem OAI.PolycyclicRecognition.bilinearCentralLattice_uniform line 51