OAI/Topology/ArtinGroups/Complexes/NegativeTwistModern.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.HomotopyEquivalence.negativeTwistModern line 17
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLayer_upperBound line 25
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLayer_lowerBound line 30
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.allPureIndex line 34
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLayer_eq_self_of_pure line 42
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLayer_idempotent line 51
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLayer_lowerTruncation line 62
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.capped_upperTruncation_far line 74
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeLayer_lowerTruncation line 81
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeLayer_top line 103
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classNegativeTwist_capped_layer line 132
12. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseWord_capped_layer line 150