OAI/Topology/ArtinGroups/Complexes/TotalVector.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classTotalVector line 16
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classSignedVector_minimal line 20
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.signedGeneratorVector_pure line 25
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classSignedVector_pure line 36
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.signedGeneratorVector_upper_partition line 43
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classSignedVector_upper_partition line 77
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.rowReflect_sub line 84
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.rowReflect_smul line 89
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.rowReflectWord_sub line 93
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.rowReflectWord_smul line 102
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classSignedVector_inverseWord line 111
12. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.canonicalLow_reflected_high_signed line 121