OAI/GroupTheory/FiniteType/SingularSigmaSingleMerge.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingularSigma.single_merge line 14
  2. lemma OAI.SingularSigma.homologyIso_single line 19
  3. lemma OAI.CWSkeletalHomology.oneDisk_maps line 34
  4. def OAI.CWSkeletalHomology.oneDisk line 42
  5. def OAI.CWSkeletalHomology.inclDisk line 46
  6. lemma OAI.CWSkeletalHomology.inclDisk_comp line 52
  7. lemma OAI.CWSkeletalHomology.diskSumIso_single line 59
  8. lemma OAI.CWSkeletalHomology.basisIso_single line 75
  9. lemma OAI.CWCellular.SkeletalMap.oneDisk_natural line 97
  10. lemma OAI.CWCellular.SkeletalMap.basis_natural line 106
  11. lemma OAI.CWEquivariant.smul_skel line 129
  12. def OAI.CWEquivariant.skeletal line 135
  13. abbrev OAI.CWEquivariant.rep line 139
  14. def OAI.CWEquivariant.orientedIso line 141
  15. lemma OAI.CWEquivariant.orientedIso_single line 145
  16. lemma OAI.CWEquivariant.orientedIso_smul line 149
  17. def OAI.CWEquivariant.boundary line 158
  18. lemma OAI.CWEquivariant.oriented_boundary line 163
  19. lemma OAI.CWEquivariant.boundary_smul line 170
  20. def OAI.CWEquivariant.boundaryIntertwiner line 177
  21. abbrev OAI.CWEquivariant.module line 180
  22. def OAI.CWEquivariant.moduleBoundary line 182
  23. lemma OAI.CWEquivariant.boundary_comp line 185
  24. lemma OAI.CWEquivariant.boundary_exact line 193