OAI/Topology/ArtinGroups/Complexes/CoconePlacement.lean
8 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.coconePlacementline 16 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.coconeDifferentialline 21 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.cocone_entriesline 25 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.cocone_degreeline 42 - lemma
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.cocone_squareline 68 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.coconeline 78 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.positiveTwistline 89 - def
OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeTwistline 93