OAI/Algebra/FrobeniusObstruction/MixedForms.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BoundaryOnly.FormalObstruction.MixedForms.Ext line 17
  2. abbrev OAI.BoundaryOnly.FormalObstruction.MixedForms.Forms line 18
  3. def OAI.BoundaryOnly.FormalObstruction.MixedForms.gen line 20
  4. def OAI.BoundaryOnly.FormalObstruction.MixedForms.wedge line 22
  5. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.wedge_apply line 25
  6. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.gen_anticommute line 28
  7. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.gen_sq line 33
  8. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.vector_supercommute line 38
  9. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.gen_supercommute line 51
  10. def OAI.BoundaryOnly.FormalObstruction.MixedForms.parity line 55
  11. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.parity_tmul line 59
  12. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.parity_sq line 63
  13. def OAI.BoundaryOnly.FormalObstruction.MixedForms.d line 71
  14. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.d_tmul line 74
  15. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.d_mul line 79
  16. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.d_parity line 96
  17. def OAI.BoundaryOnly.FormalObstruction.MixedForms.gradient line 107
  18. def OAI.BoundaryOnly.FormalObstruction.MixedForms.delta line 110
  19. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.delta_apply line 114
  20. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.antisymmetric_sum line 120
  21. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.d_sq line 133
  22. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.oneform_sq line 148
  23. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.gradient_eq line 156
  24. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.parity_gradient line 160
  25. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.delta_sq line 165
  26. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.d_delta line 170
  27. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.constant_commute line 180
  28. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.d_commutator line 188
  29. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.oneform_supercommute line 195
  30. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.gradient_supercommute line 206
  31. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.gradient_sq line 212
  32. def OAI.BoundaryOnly.FormalObstruction.MixedForms.coeff line 218
  33. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.coeff_apply line 222
  34. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.parity_coeff line 225
  35. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.coeff_commute line 229
  36. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.d_coeff line 232
  37. def OAI.BoundaryOnly.FormalObstruction.MixedForms.cartier line 236
  38. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.parity_cartier line 239
  39. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.gradient_mul_cartier line 243
  40. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.d_cartier line 247
  41. def OAI.BoundaryOnly.FormalObstruction.MixedForms.normal line 260
  42. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.normal_nil line 263
  43. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.normal_cons line 264
  44. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.d_one line 267
  45. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.d_normal line 272
  46. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.coeff_mul_normal line 279
  47. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.gradient_mul_normal line 293
  48. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.coeff_mul_normal_ideal line 304
  49. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.delta_normal line 316
  50. def OAI.BoundaryOnly.FormalObstruction.MixedForms.contract line 336
  51. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.contract_tmul line 340
  52. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.contract_coeff line 344
  53. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.contraction_identity line 351
  54. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.ambient_primitive line 366
  55. theorem OAI.BoundaryOnly.FormalObstruction.MixedForms.normal_primitive line 384