OAI/Algebra/FrobeniusObstruction/SignedTensor.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundaryOnly.FormalObstruction.SignedTensor.EndFamily line 15
  2. abbrev OAI.BoundaryOnly.FormalObstruction.SignedTensor.TensorEnd line 16
  3. def OAI.BoundaryOnly.FormalObstruction.SignedTensor.dSlot line 18
  4. def OAI.BoundaryOnly.FormalObstruction.SignedTensor.hSlot line 21
  5. def OAI.BoundaryOnly.FormalObstruction.SignedTensor.diagSlot line 24
  6. def OAI.BoundaryOnly.FormalObstruction.SignedTensor.differential line 27
  7. def OAI.BoundaryOnly.FormalObstruction.SignedTensor.homotopy line 30
  8. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.tensor_neg_at line 34
  9. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.tensor_add_at line 47
  10. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.mixed_cancel line 64
  11. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.diagonal_term line 107
  12. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.diagonal_sum line 137
  13. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.tensor_homotopy line 159
  14. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.differential_cons_tprod line 196
  15. theorem OAI.BoundaryOnly.FormalObstruction.SignedTensor.parity_cons_tprod line 209