OAI/Topology/ArtinGroups/Complexes/BasedComplexComplex.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classOfComplex line 13
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classOfComplex_eq line 18
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classOfComplex_reindex line 24
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classOfComplex_packet_reindex line 29
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classOfComplex_packet_cons line 35
6. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.exists_packetPerm line 44
7. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classPacketPerm line 83
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classPacketPerm_apply line 89