OAI/GroupTheory/PolycyclicRecognition/Geometry/TruncatedWordExponential.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The universal exponential product over truncated rational scalars

  1. abbrev OAI.PolycyclicRecognition.TruncatedWords line 16
  2. def OAI.PolycyclicRecognition.truncatedWordLetter line 21
  3. def OAI.PolycyclicRecognition.truncatedWordCoproduct line 24
  4. theorem OAI.PolycyclicRecognition.truncatedWordCoproduct_letter line 30
  5. theorem OAI.PolycyclicRecognition.truncatedWordCoproduct_parameter_letter line 37
  6. def OAI.PolycyclicRecognition.truncatedWordExponentialProduct line 45
  7. theorem OAI.PolycyclicRecognition.truncatedWordExponentialProduct_pow line 49
  8. def OAI.PolycyclicRecognition.truncatedWordLogarithm line 56
  9. theorem OAI.PolycyclicRecognition.truncatedWordLogarithm_primitive line 59