OAI/RingTheory/BassTrace/PathWeights.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.BassTrace.Paths.mapDomain_apply_of_fibre line 16
2. def OAI.BassTrace.Paths.deleteLast line 36
3. def OAI.BassTrace.Paths.insertOrbit line 41
4. lemma OAI.BassTrace.Paths.deleteLast_insertOrbit line 44
5. lemma OAI.BassTrace.Paths.insertOrbit_injective line 51
6. lemma OAI.BassTrace.Paths.deleteLast_fibre line 61
7. lemma OAI.BassTrace.Paths.pathVector_deleteLast line 79
8. def OAI.BassTrace.Paths.totalWeight line 96
9. lemma OAI.BassTrace.Paths.totalWeight_succ line 99
10. lemma OAI.BassTrace.Paths.totalWeight_eq_zeroDegree line 106
11. def OAI.BassTrace.Paths.zeroConjugate line 112
12. lemma OAI.BassTrace.Paths.zeroConjugate_mk line 114
13. lemma OAI.BassTrace.Paths.zeroConjugate_injective line 119
14. lemma OAI.BassTrace.Paths.range_zeroConjugate line 127
15. lemma OAI.BassTrace.Paths.orbitWeight_zeroDegree line 145
16. lemma OAI.BassTrace.Paths.totalWeight_finsum line 153
17. lemma OAI.BassTrace.Paths.totalWeight_conjugacy line 160
18. lemma OAI.BassTrace.Paths.twist_equivariant line 171
19. def OAI.BassTrace.Paths.orbitTwist line 180
20. lemma OAI.BassTrace.Paths.orbitIncrement_twist line 187
21. lemma OAI.BassTrace.Paths.orbitTwist_injective line 191
22. lemma OAI.BassTrace.Paths.twist_surjective line 200
23. lemma OAI.BassTrace.Paths.orbitTwist_surjective line 208
24. lemma OAI.BassTrace.Paths.orbitWeight_twist line 216
25. lemma OAI.BassTrace.Paths.pathVector_twist line 220
26. lemma OAI.BassTrace.Paths.delete_twist_tuple line 228
27. def OAI.BassTrace.Paths.deleteEntry line 239
28. lemma OAI.BassTrace.Paths.deleteEntry_zero line 245
29. lemma OAI.BassTrace.Paths.deleteEntry_castSucc_twist line 254
30. lemma OAI.BassTrace.Paths.pathVector_deleteEntry line 263