OAI/Topology/ArtinGroups/Harmonic/Level.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.GeneratorPlacement.level line 8
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.homogeneous_nonzero_degree line 16
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.positive_homogeneous_nonzero_degree line 25
4. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.differential_level line 37
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.restrict line 49
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.restrict_minimal line 74
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.differential_intermediate_level line 81
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.pureLayer_intermediate line 90
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.pureLayer line 105
10. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.pureLayer_linear line 110