OAI/GroupTheory/FiniteType/PartialResolutionPartialCyclesFg.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.PartialResolution.partial_cycles_fg line 13
  2. lemma OAI.CWEquivariant.cycles_fg line 55
  3. def OAI.CWEquivariant.absoluteRep line 75
  4. def OAI.CWEquivariant.qLinear line 97
  5. lemma OAI.CWEquivariant.qLinear_smul line 101
  6. def OAI.CWEquivariant.qRep line 115
  7. lemma OAI.CWEquivariant.qRep_boundary line 119
  8. def OAI.CWEquivariant.cyclesMap line 132
  9. lemma OAI.CWEquivariant.cyclesMap_bijective line 137
  10. def OAI.CWEquivariant.cyclesEquiv line 156
  11. def OAI.CWEquivariant.wholeRep line 170
  12. def OAI.CWEquivariant.toWhole line 184
  13. lemma OAI.CWEquivariant.toWhole_surjective line 197
  14. lemma OAI.CWEquivariant.homology_finite line 203