OAI/Topology/ArtinGroups/Complexes/OutsideCap.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.scalarExact_of_absent_degree line 14
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.testUpperBound_of_generator_cap line 23
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classTestUpper_of_generator_cap line 33
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ClassOutsideCap line 38
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classOutsideCap_of_upper line 43
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classPositiveTwist_outside_cap line 46
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classUpperBound_of_test_and_outside line 62