OAI/Topology/ArtinGroups/Complexes/HomotopyConeMap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cone_block_entries line 21
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cone_block_degree line 42
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.homotopyConeMap line 70
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homotopy_coherence_closed line 92
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cone_target_replace_backward_square line 124
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cone_target_replace_correction line 137
7. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomotopyEquivalence.coneTarget line 186