OAI/GroupTheory/FiniteType/PartialResolution.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PartialResolution.obj line 14
  2. def OAI.PartialResolution.headIso line 16
  3. def OAI.PartialResolution.tailIso line 19
  4. def OAI.PartialResolution.seam line 22
  5. def OAI.PartialResolution.d line 26
  6. lemma OAI.PartialResolution.d_head line 33
  7. lemma OAI.PartialResolution.d_seam line 37
  8. lemma OAI.PartialResolution.d_tail line 39
  9. lemma OAI.PartialResolution.d_comp line 44
  10. def OAI.PartialResolution.complex line 63
  11. lemma OAI.PartialResolution.complex_X line 66
  12. lemma OAI.PartialResolution.complex_d line 67
  13. lemma OAI.PartialResolution.exact_seam line 70
  14. lemma OAI.PartialResolution.exact_after_seam line 79
  15. def OAI.PartialResolution.startIso line 91
  16. def OAI.PartialResolution.nextIso line 94
  17. lemma OAI.PartialResolution.exactAt_succ line 97
  18. instance OAI.PartialResolution.obj_projective line 149
  19. instance OAI.PartialResolution.complex_projective line 153
  20. def OAI.PartialResolution.augmentation line 156
  21. def OAI.PartialResolution.resolution line 163
  22. lemma OAI.PartialResolution.complex_head_d line 189
  23. lemma OAI.ProductCriterion.moduleMap_comp line 206
  24. lemma OAI.ProductCriterion.moduleMap_id line 208
  25. def OAI.ProductCriterion.moduleIso line 210
  26. lemma OAI.ProductCriterion.kernel_fg_of_iso line 215