OAI/Algebra/FrobeniusObstruction/FormTensor.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundaryOnly.FormalObstruction.FormsSplit.QForms line 17
  2. def OAI.BoundaryOnly.FormalObstruction.FormsSplit.includeLeft line 20
  3. def OAI.BoundaryOnly.FormalObstruction.FormsSplit.includeRight line 23
  4. def OAI.BoundaryOnly.FormalObstruction.FormsSplit.sumEquiv line 29
  5. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.sumEquiv_symm_tmul line 35
  6. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.exterior_left_gen line 59
  7. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.exterior_right_gen line 68
  8. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.involute_map line 76
  9. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.parity_includeLeft line 86
  10. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.parity_includeRight line 93
  11. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.d_includeLeft line 102
  12. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.d_includeRight line 113
  13. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.includeLeft_coeff line 125
  14. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.includeRight_coeff line 129
  15. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.gradient_include_left line 133
  16. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.gradient_include_right line 139
  17. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.gradient_add line 145
  18. theorem OAI.BoundaryOnly.FormalObstruction.FormsSplit.delta_product line 152
  19. abbrev OAI.BoundaryOnly.FormalObstruction.GlobalForms.Coordinates line 173
  20. instance OAI.BoundaryOnly.FormalObstruction.GlobalForms.coordinatesFintype line 177
  21. instance OAI.BoundaryOnly.FormalObstruction.GlobalForms.coordinatesDecidableEq line 184
  22. abbrev OAI.BoundaryOnly.FormalObstruction.GlobalForms.consIndex line 191
  23. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.consIndex_zero line 199
  24. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.consIndex_succ line 200
  25. def OAI.BoundaryOnly.FormalObstruction.GlobalForms.tensorCons line 203
  26. theorem OAI.BoundaryOnly.FormalObstruction.GlobalForms.tensorCons_tprod line 209
  27. def OAI.BoundaryOnly.FormalObstruction.GlobalForms.emptyCoefficients line 223
  28. def OAI.BoundaryOnly.FormalObstruction.GlobalForms.emptyExterior line 231
  29. abbrev OAI.BoundaryOnly.FormalObstruction.GlobalForms.QForms line 244
  30. def OAI.BoundaryOnly.FormalObstruction.GlobalForms.emptyForms line 247
  31. def OAI.BoundaryOnly.FormalObstruction.GlobalForms.blockEquiv line 252