OAI/Algebra/FinitisticAsymmetry/Triangular/InjectiveResolution.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.CummingsConstruction.oldCharacter line 15
  2. def OAI.LittleFinitistic.CummingsConstruction.newCharacter line 18
  3. def OAI.LittleFinitistic.CummingsConstruction.newProjection line 21
  4. abbrev OAI.LittleFinitistic.CummingsConstruction.oldSimple line 28
  5. abbrev OAI.LittleFinitistic.CummingsConstruction.newSimple line 29
  6. abbrev OAI.LittleFinitistic.CummingsConstruction.newRegular line 30
  7. abbrev OAI.LittleFinitistic.CummingsConstruction.newInjectiveObj line 31
  8. def OAI.LittleFinitistic.CummingsConstruction.newRegularι line 33
  9. def OAI.LittleFinitistic.CummingsConstruction.newInjectiveπ line 51
  10. def OAI.LittleFinitistic.CummingsConstruction.newRegularπ line 58
  11. def OAI.LittleFinitistic.CummingsConstruction.newSimpleι line 65
  12. def OAI.LittleFinitistic.CummingsConstruction.newDifferential line 80
  13. def OAI.LittleFinitistic.CummingsConstruction.epsDifferential line 98
  14. lemma OAI.LittleFinitistic.CummingsConstruction.newDifferential_sq line 100
  15. lemma OAI.LittleFinitistic.CummingsConstruction.epsDifferential_sq line 106
  16. lemma OAI.LittleFinitistic.CummingsConstruction.newRegularι_comm line 112
  17. lemma OAI.LittleFinitistic.CummingsConstruction.newInjectiveπ_comm line 119
  18. lemma OAI.LittleFinitistic.CummingsConstruction.newRegularι_π line 125
  19. lemma OAI.LittleFinitistic.CummingsConstruction.newRegular_exact line 131
  20. def OAI.LittleFinitistic.CummingsConstruction.periodicInjective line 152
  21. def OAI.LittleFinitistic.CummingsConstruction.periodicRegular line 156
  22. def OAI.LittleFinitistic.CummingsConstruction.periodicOld line 160
  23. def OAI.LittleFinitistic.CummingsConstruction.periodicι line 163
  24. def OAI.LittleFinitistic.CummingsConstruction.periodicπ line 167
  25. lemma OAI.LittleFinitistic.CummingsConstruction.periodicι_π line 171
  26. lemma OAI.LittleFinitistic.CummingsConstruction.periodic_shortExact line 176
  27. lemma OAI.LittleFinitistic.CummingsConstruction.epsDifferential_π line 182
  28. lemma OAI.LittleFinitistic.CummingsConstruction.epsDifferential_exact line 188
  29. lemma OAI.LittleFinitistic.CummingsConstruction.epsDifferential_π_exact line 199
  30. instance OAI.LittleFinitistic.CummingsConstruction.newRegularπ_epi line 209
  31. def OAI.LittleFinitistic.CummingsConstruction.periodicAug line 214
  32. instance OAI.LittleFinitistic.CummingsConstruction.periodicAug_quasiIso line 218