OAI/RingTheory/BassTrace/TwistedPaths.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BassTrace.Detector.twistedRotation line 18
2. lemma OAI.BassTrace.Detector.finRotate_castSucc line 21
3. lemma OAI.BassTrace.Detector.twistedRotation_castSucc line 24
4. lemma OAI.BassTrace.Detector.twistedRotation_last line 28
5. lemma OAI.BassTrace.Detector.complex_sign_odd line 32
6. lemma OAI.BassTrace.Detector.rotation_pfaffian line 36
7. lemma OAI.BassTrace.Detector.twisted_pfaffian line 46
8. def OAI.BassTrace.Paths.weightedSum line 79
9. lemma OAI.BassTrace.Paths.weightedSum_congr line 82
10. lemma OAI.BassTrace.Paths.weightedSum_add line 86
11. lemma OAI.BassTrace.Paths.weightedSum_neg line 90
12. lemma OAI.BassTrace.Paths.weightedSum_sum line 94
13. lemma OAI.BassTrace.Paths.weightedSum_const_mul line 99
14. lemma OAI.BassTrace.Paths.weightedSum_mapDomain line 106
15. lemma OAI.BassTrace.Paths.weightedSum_twist line 112
16. lemma OAI.BassTrace.Paths.weightedSum_deleteEntry line 117
17. lemma OAI.BassTrace.Detector.twist_eq_twistedRotation line 135
18. def OAI.BassTrace.Detector.orbitPfaffian line 145
19. def OAI.BassTrace.Detector.orbitDetector line 152
20. lemma OAI.BassTrace.Detector.orbitPfaffian_twist line 159
21. def OAI.BassTrace.Detector.pfaffianSum line 172
22. def OAI.BassTrace.Detector.detectorSum line 176
23. lemma OAI.BassTrace.Detector.pfaffianSum_twist line 179
24. lemma OAI.BassTrace.Detector.pfaffian_zero line 200
25. lemma OAI.BassTrace.Detector.detector_zero line 208
26. lemma OAI.BassTrace.Detector.alternating_sum_odd line 213
27. lemma OAI.BassTrace.Detector.orbitDetector_zero line 225
28. lemma OAI.BassTrace.Detector.orbitDetector_succ line 230
29. lemma OAI.BassTrace.Detector.detectorSum_eq_pfaffianSum line 239
30. lemma OAI.BassTrace.Detector.pfaffianSum_recurrence line 258
31. lemma OAI.BassTrace.Detector.pfaffianSum_value line 264
32. lemma OAI.BassTrace.Detector.detectorSum_value line 276