OAI/GroupTheory/PolycyclicRecognition/Algebra/SubexponentialOperations.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Powers, sums, minima and reciprocals of subexponential bounds

  1. theorem OAI.PolycyclicRecognition.HasSubexponentialLowerBound.pow line 12
  2. theorem OAI.PolycyclicRecognition.HasSubexponentialLowerBound.min line 19
  3. theorem OAI.PolycyclicRecognition.HasSubexponentialLowerBound.inv line 26
  4. theorem OAI.PolycyclicRecognition.HasSubexponentialUpperBound.pow line 36
  5. theorem OAI.PolycyclicRecognition.HasSubexponentialUpperBound.add line 44