OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalCoefficientSequence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The factorial coefficient system with colimit the rational numbers

  1. def OAI.PolycyclicRecognition.factorialMultiplier line 12
  2. theorem OAI.PolycyclicRecognition.factorialMultiplier_comp line 14
  3. theorem OAI.PolycyclicRecognition.factorialMultiplier_self line 19
  4. theorem OAI.PolycyclicRecognition.factorialMultiplier_zero line 22
  5. theorem OAI.PolycyclicRecognition.factorialMultiplier_factorial line 26
  6. def OAI.PolycyclicRecognition.rationalCoefficientDiagram line 31
  7. def OAI.PolycyclicRecognition.rationalCoefficientInclusion line 39
  8. theorem OAI.PolycyclicRecognition.rationalCoefficientInclusion_apply line 47
  9. def OAI.PolycyclicRecognition.rationalCoefficientColimit line 50