OAI/Topology/ArtinGroups/Complexes/PlacementSignedWeight.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.placementSignedWeight line 15
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.signedGeneratorVector line 18
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.signedGeneratorVector_array line 23
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.signedGeneratorVector_minimal_eq line 31
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.signedWeight_cancel line 41
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarPivot.signedGeneratorVector_reduced line 52
7. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.FiniteModel.exists_minimal_signed line 75
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.FiniteModel.signedGeneratorVector_homotopy line 101
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classSignedVector line 112
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classSignedVector_mk line 117