OAI/Algebra/FinitisticAsymmetry/Derived/Telescopes.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LittleFinitistic.DerivedSupport.telescopeMap line 18
  2. lemma OAI.LittleFinitistic.DerivedSupport.telescopeMap_inj line 22
  3. def OAI.LittleFinitistic.DerivedSupport.telescopeπ line 26
  4. lemma OAI.LittleFinitistic.DerivedSupport.telescopeπ_inj line 31
  5. lemma OAI.LittleFinitistic.DerivedSupport.telescope_zero line 34
  6. def OAI.LittleFinitistic.DerivedSupport.telescopeCokernel line 44
  7. abbrev OAI.LittleFinitistic.DerivedSupport.moduleTelescopeMap line 78
  8. def OAI.LittleFinitistic.DerivedSupport.moduleTelescopeLinear line 80
  9. lemma OAI.LittleFinitistic.DerivedSupport.moduleTelescope_at_zero line 83
  10. lemma OAI.LittleFinitistic.DerivedSupport.moduleTelescope_at_succ line 103
  11. instance OAI.LittleFinitistic.DerivedSupport.moduleTelescopeMap_mono line 127
  12. def OAI.LittleFinitistic.DerivedSupport.moduleTelescopeShortComplex line 150
  13. lemma OAI.LittleFinitistic.DerivedSupport.moduleTelescope_shortExact line 155
  14. lemma OAI.LittleFinitistic.DerivedSupport.localizing_sequence_colimit line 163