OAI/GroupTheory/PeriodicGroups/Frames/AcyclicFrameEdge.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SourceBurnside.Stability.HomologyEdge.Z line 12
  2. def OAI.SourceBurnside.Stability.HomologyEdge.ontoCycles line 14
  3. lemma OAI.SourceBurnside.Stability.HomologyEdge.ontoCycles_epi line 17
  4. def OAI.SourceBurnside.Stability.HomologyEdge.cycleSequence line 20
  5. lemma OAI.SourceBurnside.Stability.HomologyEdge.cycleSequence_exact line 25
  6. lemma OAI.SourceBurnside.Stability.HomologyEdge.cycleSequence_shortExact line 49
  7. lemma OAI.SourceBurnside.Stability.HomologyEdge.zero_H0_of_epi line 56
  8. lemma OAI.SourceBurnside.Stability.HomologyEdge.isIso_H2_augmentation line 61
  9. def OAI.SourceBurnside.Stability.Frames.differentialRep line 108
  10. lemma OAI.SourceBurnside.Stability.Frames.differentialRep_val line 117
  11. def OAI.SourceBurnside.Stability.Frames.repComplex line 120
  12. lemma OAI.SourceBurnside.Stability.Frames.repComplex_d line 130
  13. lemma OAI.SourceBurnside.Stability.Frames.repComplex_exact line 134
  14. lemma OAI.SourceBurnside.Stability.Frames.differentialRep_epi line 150
  15. lemma OAI.SourceBurnside.Stability.Frames.degreeZero_scalar line 158
  16. def OAI.SourceBurnside.Stability.Frames.degreeZeroIso line 175
  17. def OAI.SourceBurnside.Stability.Frames.Index line 215
  18. lemma OAI.SourceBurnside.Stability.Frames.span_index line 217
  19. def OAI.SourceBurnside.Stability.Frames.frameBasis line 228
  20. lemma OAI.SourceBurnside.Stability.Frames.frameBasis_val line 232
  21. def OAI.SourceBurnside.Stability.Frames.indexAction line 240
  22. lemma OAI.SourceBurnside.Stability.Frames.indexAction_val line 252
  23. lemma OAI.SourceBurnside.Stability.Frames.frame_action_monomial line 256
  24. def OAI.SourceBurnside.Stability.Frames.labelHom line 273
  25. lemma OAI.SourceBurnside.Stability.Frames.labelHom_vertex line 276
  26. lemma OAI.SourceBurnside.Stability.Frames.labelHom_id line 280
  27. lemma OAI.SourceBurnside.Stability.Frames.labelHom_comp line 283
  28. lemma OAI.SourceBurnside.Stability.Frames.labelHom_basis line 289
  29. def OAI.SourceBurnside.Stability.Frames.labelEquiv line 303
  30. lemma OAI.SourceBurnside.Stability.Frames.labelHom_chains line 319
  31. def OAI.SourceBurnside.Stability.Frames.chainLinear line 334
  32. def OAI.SourceBurnside.Stability.Frames.chainEquiv line 341
  33. lemma OAI.SourceBurnside.Stability.Frames.chainEquiv_intertwining line 353
  34. def OAI.SourceBurnside.Stability.Frames.chainHomologyIso line 365