OAI/GroupTheory/PolycyclicRecognition/Finiteness/HorseshoeProjectiveTowers.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Three compatible projective towers resolving a short exact sequence

  1. def OAI.PolycyclicRecognition.horseshoeStage line 13
  2. def OAI.PolycyclicRecognition.horseshoeLeftTower line 20
  3. def OAI.PolycyclicRecognition.horseshoeMiddleTower line 30
  4. def OAI.PolycyclicRecognition.horseshoeRightTower line 46
  5. def OAI.PolycyclicRecognition.horseshoeTowerInl line 56
  6. def OAI.PolycyclicRecognition.horseshoeTowerSnd line 63
  7. theorem OAI.PolycyclicRecognition.horseshoeTower_zero line 70
  8. theorem OAI.PolycyclicRecognition.horseshoeTower_shortExact line 74