OAI/Topology/ArtinGroups/Complexes/InverseTwistIdentity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistProjection_commute line 14
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistInjection_commute line 32
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwist_targetEquation line 52
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistIdentity line 63
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwistIdentity_eq line 76
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.unitContraction_entries line 86
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.testToken_entries line 97
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.inverseTwist_sourceEquation line 114