OAI/GroupTheory/SimpleAmenable/Homology/BiProjective.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BiResolution.aug₀ line 16
  2. lemma OAI.BiResolution.ι_aug₀ line 22
  3. lemma OAI.BiResolution.d_aug₀ line 29
  4. def OAI.BiResolution.pi line 69
  5. lemma OAI.BiResolution.pi_f_zero line 72
  6. def OAI.BiResolution.evalComplexIso line 74
  7. def OAI.BiResolution.evalTotalIso line 86
  8. lemma OAI.BiResolution.contraction_aug line 102
  9. lemma OAI.BiResolution.eval_inverse_aug line 133
  10. instance OAI.BiResolution.pi_quasiIso line 148
  11. def OAI.BiResolution.resolution line 171
  12. lemma OAI.ModelAssembly.pre_forward line 189
  13. def OAI.ModelAssembly.models line 211
  14. def OAI.ModelAssembly.freeNatIso line 217
  15. def OAI.ModelAssembly.modelEquiv line 220
  16. def OAI.ModelAssembly.assembledEquiv line 223