OAI/Algebra/FrobeniusObstruction/TensorCohomology.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.tensor_map_zero_at line 18
  2. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.representatives_cycles line 25
  3. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.projection_boundaries line 39
  4. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.tensor_cycle_decomposition line 55
  5. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.tensor_representatives_injective_mod_boundaries line 82
  6. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.project_differential line 106
  7. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.project_tensor_map line 135