OAI/RingTheory/BassTrace/PfaffianDetector.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

Alternating functions on vertex labels extend to oriented exterior chains.

  1. lemma OAI.BassTrace.Detector.rawTwoForm_map line 16
  2. lemma OAI.BassTrace.Detector.twoForm_row line 23
  3. lemma OAI.BassTrace.Detector.multiplyVector_pfaffian_minor line 60
  4. lemma OAI.BassTrace.Detector.detector_pfaffian_sum line 76
  5. lemma OAI.BassTrace.Detector.twoForm_eq_upper line 92
  6. instance OAI.BassTrace.Oriented.(instance at line 145) line 145
  7. lemma OAI.BassTrace.Detector.scalar_alt_zero line 158
  8. def OAI.BassTrace.Detector.pfaffianAlt line 176
  9. def OAI.BassTrace.Detector.detectorAlt line 183
  10. def OAI.BassTrace.Detector.cocycle line 196
  11. lemma OAI.BassTrace.Detector.cocycle_wedge line 199
  12. lemma OAI.BassTrace.Detector.cocycle_eq_coboundary line 203
  13. lemma OAI.BassTrace.Detector.cocycle_closed line 213
  14. lemma OAI.BassTrace.Detector.cocycle_lift_independent line 218