OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianRealSpace.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The real abelian coordinate space and its explicit integer lattice

  1. def OAI.PolycyclicRecognition.AbelianRealSpace line 11
  2. instance OAI.PolycyclicRecognition.abelianRealNormedLie line 13
  3. instance OAI.PolycyclicRecognition.abelianRealFiniteDimensional line 36
  4. instance OAI.PolycyclicRecognition.abelianRealLieAbelian line 39
  5. instance OAI.PolycyclicRecognition.abelianRealCoordinates line 42
  6. instance OAI.PolycyclicRecognition.abelianRealCommGroup line 45
  7. def OAI.PolycyclicRecognition.abelianRealLattice line 48
  8. theorem OAI.PolycyclicRecognition.abelianRealLattice_uniform line 51
  9. def OAI.PolycyclicRecognition.abelianRealLatticeMap line 54
  10. def OAI.PolycyclicRecognition.abelianRealLatticeEquiv line 59
  11. theorem OAI.PolycyclicRecognition.abelianRealLatticeEquiv_apply line 66