OAI/GroupTheory/PolycyclicRecognition/Algebra/TwistedBilateralDifference.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Removing the coefficient twist from a bilateral shift

  1. def OAI.PolycyclicRecognition.bilateralPowerMap line 13
  2. theorem OAI.PolycyclicRecognition.bilateralPowerMap_single line 16
  3. theorem OAI.PolycyclicRecognition.bilateralPowerMap_inv_comp line 20
  4. def OAI.PolycyclicRecognition.bilateralGauge line 31
  5. theorem OAI.PolycyclicRecognition.bilateralGauge_single line 36
  6. def OAI.PolycyclicRecognition.twistedBilateralShift line 41
  7. theorem OAI.PolycyclicRecognition.twistedBilateralShift_single line 45
  8. theorem OAI.PolycyclicRecognition.bilateralGauge_shift line 49
  9. def OAI.PolycyclicRecognition.twistedBilateralDifference line 64
  10. def OAI.PolycyclicRecognition.twistedBilateralSum line 67
  11. theorem OAI.PolycyclicRecognition.bilateralGauge_difference line 70
  12. theorem OAI.PolycyclicRecognition.twistedBilateralDifference_injective line 77
  13. theorem OAI.PolycyclicRecognition.twistedBilateralSum_surjective line 84
  14. theorem OAI.PolycyclicRecognition.twistedBilateralSum_ker_eq_range line 88