OAI/GroupTheory/PolycyclicRecognition/Algebra/RepCofiber.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

Coordinates on the mapping cone used for cyclic extensions

  1. theorem OAI.PolycyclicRecognition.rep_shortComplex_exact_iff line 17
  2. abbrev OAI.PolycyclicRecognition.repCofiber line 29
  3. abbrev OAI.PolycyclicRecognition.repCofiberFst line 30
  4. abbrev OAI.PolycyclicRecognition.repCofiberSnd line 32
  5. abbrev OAI.PolycyclicRecognition.repCofiberInl line 34
  6. abbrev OAI.PolycyclicRecognition.repCofiberInr line 36
  7. theorem OAI.PolycyclicRecognition.repCofiber_zero_decompose line 39
  8. theorem OAI.PolycyclicRecognition.repCofiber_ext_zero line 43
  9. theorem OAI.PolycyclicRecognition.repCofiber_decompose line 47
  10. theorem OAI.PolycyclicRecognition.repCofiber_snd_d line 63
  11. theorem OAI.PolycyclicRecognition.repCofiber_fst_d line 69
  12. theorem OAI.PolycyclicRecognition.repCofiber_fst_inl line 75
  13. theorem OAI.PolycyclicRecognition.repCofiber_snd_inl line 79
  14. theorem OAI.PolycyclicRecognition.repCofiber_fst_inr line 83
  15. theorem OAI.PolycyclicRecognition.repCofiber_snd_inr line 87
  16. theorem OAI.PolycyclicRecognition.repCofiber_ext line 91