OAI/Topology/ArtinGroups/Complexes/NegativeAmplitudeCoreIndex.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.NegativeAmplitudeCoreIndex line 13
2. instance OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeAmplitudeCoreFintype line 17
3. instance OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeAmplitudeCoreDecidable line 23
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.tokenTest line 26
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.tokenTest_injective line 31
6. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeAmplitudeIndexMap line 36
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeAmplitudeIndexMap_injective line 45
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeAmplitudeIndexMap_surjective line 65
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeAmplitudeIndexEquiv line 78
10. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.normalizedNegativeAmplitudeTwist line 84
11. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeAmplitudePivot line 89
12. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.reducedNegativeAmplitudeTwist line 107
13. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.negativeAmplitudeTwistReduction line 111
14. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.reducedNegativeAmplitudeTwist_placement line 116