OAI/Topology/ArtinGroups/Complexes/PacketPermReindex.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classPacketPerm_reindexline 14 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classPacketPerm_emptyline 25 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classPacketPerm_consline 36 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classPacketPerm_sumline 54 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classPacketPerm_inverse_sumline 83