OAI/GroupTheory/PolycyclicRecognition/Analysis/ChainSuccessor.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

The successor shift of a nonnegative chain complex

  1. def OAI.PolycyclicRecognition.negativeChainComplex line 16
  2. def OAI.PolycyclicRecognition.chainModuleNegIdentityIso line 24
  3. def OAI.PolycyclicRecognition.negativeChainShortComplexIso line 30
  4. def OAI.PolycyclicRecognition.negativeChainHomologyIso line 38
  5. def OAI.PolycyclicRecognition.chainSuccessorEmbedding line 42
  6. def OAI.PolycyclicRecognition.chainSuccessor line 47
  7. def OAI.PolycyclicRecognition.chainSuccessorXIso line 51
  8. def OAI.PolycyclicRecognition.chainSuccessorHomologyIso line 55
  9. theorem OAI.PolycyclicRecognition.chainSuccessor_zero line 60
  10. theorem OAI.PolycyclicRecognition.chainSuccessor_homology_zero line 66
  11. theorem OAI.PolycyclicRecognition.chainSuccessor_d line 72
  12. def OAI.PolycyclicRecognition.chainSuccessorCyclesIso line 78
  13. theorem OAI.PolycyclicRecognition.chainSuccessorCyclesIso_iCycles line 83
  14. theorem OAI.PolycyclicRecognition.chainSuccessorHomologyIso_π line 97