OAI/GroupTheory/PolycyclicRecognition/Lattices/IntegralLatticeGenerators.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Coordinate generators and the standard embedding of the integral lattice

  1. def OAI.PolycyclicRecognition.integralLatticeGenerator line 10
  2. theorem OAI.PolycyclicRecognition.integralLatticeGenerator_prod line 13
  3. theorem OAI.PolycyclicRecognition.integralLatticeGenerator_closure line 20
  4. theorem OAI.PolycyclicRecognition.integralLattice_hom_ext line 28
  5. def OAI.PolycyclicRecognition.integerVectorHom line 35
  6. theorem OAI.PolycyclicRecognition.integerVectorHom_injective line 40
  7. def OAI.PolycyclicRecognition.integerVectorRangeEquiv line 44
  8. theorem OAI.PolycyclicRecognition.integerVectorHom_range line 49
  9. theorem OAI.PolycyclicRecognition.integerVectorHom_uniform line 61