OAI/Topology/ArtinGroups/Complexes/ActedIndex.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ActedIndex line 17
2. abbrev OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.AmplitudeCoreIndex line 20
3. instance OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.amplitudeCoreFintype line 24
4. instance OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.amplitudeCoreDecidable line 30
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.unitTest line 33
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.unitTest_injective line 38
7. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.amplitudeIndexMap line 43
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.amplitudeIndexMap_injective line 52
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.amplitudeIndexMap_surjective line 72
10. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.amplitudeIndexEquiv line 85
11. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.normalizedAmplitudeTwist line 91
12. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.amplitudePivot line 96
13. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.reducedAmplitudeTwist line 113
14. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.amplitudeTwistReduction line 117
15. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.reducedAmplitudeTwist_placement line 122