OAI/Algebra/FiniteTensor/ExteriorForms.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

Exterior forms, differentials, Koszul operators and residue pairings.

  1. abbrev OAI.PD4Tensor.Forms.E line 17
  2. abbrev OAI.PD4Tensor.Forms.Ω line 18
  3. def OAI.PD4Tensor.Forms.dx line 20
  4. def OAI.PD4Tensor.Forms.scalar line 21
  5. def OAI.PD4Tensor.Forms.parity line 22
  6. def OAI.PD4Tensor.Forms.oneForm line 25
  7. theorem OAI.PD4Tensor.Forms.parity_tmul line 30
  8. theorem OAI.PD4Tensor.Forms.parity_dx line 34
  9. theorem OAI.PD4Tensor.Forms.parity_parity line 39
  10. theorem OAI.PD4Tensor.Forms.exterior_anticommute line 46
  11. theorem OAI.PD4Tensor.Forms.oneForm_anticommute line 57
  12. theorem OAI.PD4Tensor.Forms.parity_oneForm line 68
  13. theorem OAI.PD4Tensor.Forms.oneForm_sq_zero line 73
  14. def OAI.PD4Tensor.Forms.differential line 84
  15. theorem OAI.PD4Tensor.Forms.differential_tmul line 88
  16. theorem OAI.PD4Tensor.Forms.differential_scalar line 92
  17. theorem OAI.PD4Tensor.Forms.parity_scalar line 97
  18. theorem OAI.PD4Tensor.Forms.differential_mul line 100
  19. theorem OAI.PD4Tensor.Forms.differential_parity line 118
  20. theorem OAI.PD4Tensor.Forms.differential_sq_zero line 126
  21. theorem OAI.PD4Tensor.Forms.scalar_mul line 150
  22. theorem OAI.PD4Tensor.Forms.scalar_add line 154
  23. theorem OAI.PD4Tensor.Forms.scalar_zero line 158
  24. theorem OAI.PD4Tensor.Forms.scalar_one line 160
  25. theorem OAI.PD4Tensor.Forms.scalar_commute line 164
  26. def OAI.PD4Tensor.Forms.contraction line 171
  27. theorem OAI.PD4Tensor.Forms.contraction_tmul line 176
  28. theorem OAI.PD4Tensor.Forms.contraction_oneForm_mul line 180
  29. theorem OAI.PD4Tensor.Forms.gradient_multiple_boundary line 192
  30. def OAI.PD4Tensor.Forms.normalFactor line 211
  31. def OAI.PD4Tensor.Forms.normalCycle line 214
  32. theorem OAI.PD4Tensor.Forms.deriv_one_eq_zero line 225
  33. theorem OAI.PD4Tensor.Forms.differential_one line 232
  34. theorem OAI.PD4Tensor.Forms.differential_power_mul_self line 237
  35. theorem OAI.PD4Tensor.Forms.normalFactor_closed line 252
  36. theorem OAI.PD4Tensor.Forms.normalCycle_closed line 259
  37. theorem OAI.PD4Tensor.Forms.normalFactor_scalar_ann line 270
  38. theorem OAI.PD4Tensor.Forms.normalFactor_dscalar_ann line 275
  39. theorem OAI.PD4Tensor.Forms.normalCycle_scalar_ann line 281
  40. theorem OAI.PD4Tensor.Forms.normalCycle_dscalar_ann line 293
  41. theorem OAI.PD4Tensor.Forms.normalCycle_ideal_ann line 308
  42. theorem OAI.PD4Tensor.Forms.gradient_ideal_boundary line 329
  43. theorem OAI.PD4Tensor.Forms.oneForm_mul_zero_iff line 338
  44. theorem OAI.PD4Tensor.Forms.boundary_mul_cycle_zero line 353