OAI/GroupTheory/PolycyclicRecognition/Lattices/VectorLatticeModel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The integral vector lattice as a solvable Lie lattice

This constructs the abelian case of the lattice-realization input. The compact fundamental cover is the closed unit parallelepiped of the standard real basis.

  1. def OAI.PolycyclicRecognition.vectorSolvableLieModel line 20
  2. def OAI.PolycyclicRecognition.standardVectorLattice line 35
  3. theorem OAI.PolycyclicRecognition.standardVectorLattice_uniform line 38
  4. def OAI.PolycyclicRecognition.standardVectorLatticeEquiv line 57
  5. theorem OAI.PolycyclicRecognition.integralLattice_solvable_realization line 84