OAI/Topology/ArtinGroups/Cancellation/ScalarPivot.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.homogeneous_smul line 13
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.projectiveEntries_single line 20
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mapDegree_single line 29
4. structure OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot line 52
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.scalarPivot_of_not_minimal line 64
6. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.inverseValue line 73
7. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.homotopy line 76
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.inverseValue_left line 80
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.inverseValue_right line 86
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.inverseValue_entry line 92
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.entry_inverseValue line 98
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.homotopy_entries line 103
13. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.homotopy_degree line 106
14. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.homotopy_square line 114
15. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.homotopy_retract line 117
16. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.remainder line 121
17. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.remainder_entries line 125
18. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.remainder_degree line 133
19. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.remainder_commutes line 142
20. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.remainder_square line 146
21. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.remainder_source_row line 154
22. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.remainder_target_column line 166
23. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.remainder_retained line 178