OAI/GroupTheory/PolycyclicRecognition/Geometry/ExponentialTupleCoordinates.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Exact product volume under independent exponential coordinate charts

  1. def OAI.PolycyclicRecognition.basisVolumeMultiplier line 19
  2. def OAI.PolycyclicRecognition.exponentialBasisHomeomorph line 22
  3. theorem OAI.PolycyclicRecognition.exponentialBasisHomeomorph_apply line 29
  4. theorem OAI.PolycyclicRecognition.map_exponentialBasisHomeomorph_inverse line 36
  5. theorem OAI.PolycyclicRecognition.map_exponential_tuple_coordinates line 57
  6. def OAI.PolycyclicRecognition.exponentialTupleCoordinates line 80
  7. theorem OAI.PolycyclicRecognition.exponential_tuple_subset_measure line 86