OAI/RingTheory/BassTrace/ExteriorDetector.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

Exterior identities for the lift-independent Pfaffian detector.

  1. lemma OAI.BassTrace.Detector.ι_mul_ι_neg line 20
  2. lemma OAI.BassTrace.Detector.ι_commute_two line 25
  3. lemma OAI.BassTrace.Detector.ι_commute_degree_two line 38
  4. lemma OAI.BassTrace.Detector.gauge_invariance line 52
  5. abbrev OAI.BassTrace.Detector.CoordinateSpace line 77
  6. abbrev OAI.BassTrace.Detector.CoordinateAlgebra line 79
  7. def OAI.BassTrace.Detector.coordinate line 81
  8. def OAI.BassTrace.Detector.coordinateVector line 83
  9. def OAI.BassTrace.Detector.rawTwoForm line 85
  10. def OAI.BassTrace.Detector.twoForm line 88
  11. lemma OAI.BassTrace.Detector.rawTwoForm_add line 90
  12. lemma OAI.BassTrace.Detector.rawTwoForm_sub line 94
  13. lemma OAI.BassTrace.Detector.rawTwoForm_rank_one line 98
  14. lemma OAI.BassTrace.Detector.twoForm_add line 110
  15. lemma OAI.BassTrace.Detector.twoForm_decomposable line 114
  16. lemma OAI.BassTrace.Detector.twoForm_mem line 121
  17. lemma OAI.BassTrace.Detector.twoForm_lift_change line 132
  18. lemma OAI.BassTrace.Detector.detector_form_lift_independent line 140
  19. def OAI.BassTrace.Detector.coordinateMap line 148
  20. lemma OAI.BassTrace.Detector.coordinateMap_coordinate line 152
  21. lemma OAI.BassTrace.Detector.coordinateMap_vector line 155
  22. lemma OAI.BassTrace.Detector.twoForm_map line 161
  23. abbrev OAI.BassTrace.Detector.coordinateBasis line 181
  24. def OAI.BassTrace.Detector.topIndex line 184
  25. lemma OAI.BassTrace.Detector.topIndex_val line 187
  26. lemma OAI.BassTrace.Detector.topIndex_unique line 194
  27. abbrev OAI.BassTrace.Detector.topBasis line 201
  28. def OAI.BassTrace.Detector.topVolume line 203
  29. lemma OAI.BassTrace.Detector.topBasis_topIndex line 206
  30. def OAI.BassTrace.Detector.topCoefficient line 211
  31. lemma OAI.BassTrace.Detector.topCoefficient_topVolume line 214
  32. lemma OAI.BassTrace.Detector.top_scalar line 219
  33. lemma OAI.BassTrace.Detector.homogeneous_mul line 233
  34. lemma OAI.BassTrace.Detector.homogeneous_pow line 240
  35. def OAI.BassTrace.Detector.pfaffian line 249
  36. lemma OAI.BassTrace.Detector.topVolume_map_perm line 253
  37. lemma OAI.BassTrace.Detector.topCoefficient_map_perm line 263
  38. lemma OAI.BassTrace.Detector.exteriorMap_coe line 274
  39. def OAI.BassTrace.Detector.multiplyVector line 287
  40. lemma OAI.BassTrace.Detector.multiplyVector_coe line 296
  41. def OAI.BassTrace.Detector.insertCoordinate line 300
  42. lemma OAI.BassTrace.Detector.insertCoordinate_topVolume line 304
  43. lemma OAI.BassTrace.Detector.topCoefficient_insertCoordinate line 322
  44. def OAI.BassTrace.Detector.pfaffianForm line 329
  45. def OAI.BassTrace.Detector.detectorForm line 334
  46. def OAI.BassTrace.Detector.detector line 338
  47. lemma OAI.BassTrace.Detector.detector_lift_independent line 341
  48. lemma OAI.BassTrace.Detector.pfaffianForm_map line 348
  49. lemma OAI.BassTrace.Detector.detectorForm_map line 355
  50. lemma OAI.BassTrace.Detector.pfaffian_perm line 364
  51. lemma OAI.BassTrace.Detector.detector_perm line 371