OAI/Topology/ArtinGroups/Complexes/WordInverseModel.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.wordInverseModel line 13
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.wordLowModel line 16
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.canonicalLowSource line 20
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.canonicalLowTarget line 22
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.canonicalLowMap line 25
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.canonicalLowSource_class line 31
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.canonicalLowTarget_class line 36
8. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.canonicalLowMap_homMono line 45
9. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.canonicalReducedWordLow_subobject line 67