OAI/Topology/ArtinGroups/Complexes/LowMatrix.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowMatrix line 16
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowMatrix_mul line 22
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowMatrix_add line 41
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowMatrix_identity line 46
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.lowerTruncation line 54
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homotopy_level_bound line 68
7. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomotopyEquivalence.lowerTruncation line 74
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.lowInclusion_natural line 106