OAI/Topology/ArtinGroups/Cancellation/BlockPivot.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot line 12
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.homotopy line 27
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.homotopy_entries line 33
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.homotopy_degree line 53
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.homotopy_mul line 77
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.mul_homotopy line 91
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.homotopy_square line 108
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.homotopy_retract line 118
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.remainder line 136
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.remainder_entries line 140
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.remainder_degree line 148
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.remainder_commutes line 157
13. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.remainder_square line 161
14. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.remainder_source_row line 169
15. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.remainder_target_column line 181
16. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.remainder_retained line 198
17. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.BlockPivot.retained_sum line 210