OAI/Algebra/FrobeniusObstruction/GlobalForms.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.blockEquiv_succ_symm_tensorCons line 14
  2. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.blockEquiv_succ_symm_tprod line 26
  3. def OAI.BoundaryOnly.FormalObstruction.GlobalForms.potential line 40
  4. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.parity_empty line 54
  5. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.blockEquiv_symm_parity line 69
  6. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.blockEquiv_succ_symm_differential_tprod line 95
  7. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.blockEquiv_symm_d line 120
  8. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.blockEquiv_symm_delta line 147
  9. def OAI.BoundaryOnly.FormalObstruction.GlobalForms.insertScalar line 182
  10. def OAI.BoundaryOnly.FormalObstruction.GlobalForms.insertForms line 192
  11. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.includeLeft_coeff line 199
  12. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.includeRight_coeff line 204
  13. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.insertForms_coeff line 209
  14. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.potential_sum line 223
  15. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.blockEquiv_symm_tprod_prod line 233
  16. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.d_insertForms line 253
  17. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.gradient_insertScalar line 268
  18. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.delta_insertForms line 275
  19. def OAI.BoundaryOnly.FormalObstruction.GlobalForms.sigmaSucc line 289
  20. def OAI.BoundaryOnly.FormalObstruction.GlobalForms.coordinateEquiv line 296
  21. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.coordinateEquiv_zero line 301
  22. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.coordinateEquiv_succ line 304
  23. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.coordinateEquiv_symm_zero line 310
  24. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.coordinateEquiv_symm_succ line 313
  25. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.insertScalar_coordinate line 319