OAI/Topology/ArtinGroups/Complexes/ExtendLayer.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.tokenOnly_mul_positive line 10
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.positive_mul_tokenOnly line 23
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.differential_arrow_level line 39
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.extendLayer line 49
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.extendLayer_entry line 74
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.extendLayer_apply line 81
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.extendLayer_linear line 90
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.extendLayer_homSpace line 101