OAI/Algebra/FrobeniusObstruction/BlockCohomology.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundaryOnly.FormalObstruction.BlockCohomology.H line 17
  2. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.delta_parity line 19
  3. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.delta_d line 24
  4. def OAI.BoundaryOnly.FormalObstruction.BlockCohomology.P line 28
  5. def OAI.BoundaryOnly.FormalObstruction.BlockCohomology.D line 31
  6. def OAI.BoundaryOnly.FormalObstruction.BlockCohomology.coefficient line 34
  7. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.coefficient_apply line 38
  8. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.delta_coefficient line 41
  9. def OAI.BoundaryOnly.FormalObstruction.BlockCohomology.S line 46
  10. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.P_sq line 49
  11. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.D_sq line 55
  12. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.D_P line 59
  13. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.S_P line 67
  14. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.retraction line 78
  15. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.correction line 90