OAI/Algebra/FrobeniusObstruction/BlockTensor.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BoundaryOnly.FormalObstruction.BlockCohomology.Contraction line 17
  2. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.contraction_exists line 30
  3. def OAI.BoundaryOnly.FormalObstruction.BlockCohomology.contraction line 35
  4. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.Contraction.class_j line 41
  5. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.Contraction.project_odd line 45
  6. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.Contraction.project_even line 51
  7. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.Contraction.project_d line 57
  8. theorem OAI.BoundaryOnly.FormalObstruction.BlockCohomology.Contraction.project_coefficient line 61
  9. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.differential_map line 73
  10. abbrev OAI.BoundaryOnly.FormalObstruction.BlockTensor.V line 102
  11. abbrev OAI.BoundaryOnly.FormalObstruction.BlockTensor.H line 105
  12. def OAI.BoundaryOnly.FormalObstruction.BlockTensor.P line 106
  13. def OAI.BoundaryOnly.FormalObstruction.BlockTensor.D line 108
  14. def OAI.BoundaryOnly.FormalObstruction.BlockTensor.delta line 109
  15. def OAI.BoundaryOnly.FormalObstruction.BlockTensor.S line 110
  16. def OAI.BoundaryOnly.FormalObstruction.BlockTensor.HP line 112
  17. def OAI.BoundaryOnly.FormalObstruction.BlockTensor.HD line 113
  18. def OAI.BoundaryOnly.FormalObstruction.BlockTensor.HS line 115
  19. def OAI.BoundaryOnly.FormalObstruction.BlockTensor.j line 118
  20. def OAI.BoundaryOnly.FormalObstruction.BlockTensor.p line 120
  21. theorem OAI.BoundaryOnly.FormalObstruction.BlockTensor.projection_boundary line 123
  22. theorem OAI.BoundaryOnly.FormalObstruction.BlockTensor.representatives_cycle line 128
  23. theorem OAI.BoundaryOnly.FormalObstruction.BlockTensor.cycle_decomposition line 133
  24. theorem OAI.BoundaryOnly.FormalObstruction.BlockTensor.project_parity line 152
  25. theorem OAI.BoundaryOnly.FormalObstruction.BlockTensor.project_D line 158
  26. theorem OAI.BoundaryOnly.FormalObstruction.BlockTensor.project_S line 167
  27. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.differential_anticomm line 186
  28. theorem OAI.BoundaryOnly.FormalObstruction.BlockTensor.D_delta_anticomm line 217
  29. theorem OAI.BoundaryOnly.FormalObstruction.BlockTensor.S_delta_comm line 238
  30. theorem OAI.BoundaryOnly.FormalObstruction.BlockTensor.project_D_cycle line 273
  31. theorem OAI.BoundaryOnly.FormalObstruction.BlockTensor.pairing_project_D line 286
  32. theorem OAI.BoundaryOnly.FormalObstruction.BlockTensor.project_S_cycle line 303
  33. theorem OAI.BoundaryOnly.FormalObstruction.BlockTensor.selected_classes line 319
  34. theorem OAI.BoundaryOnly.FormalObstruction.BlockTensor.selected_cycles line 362