OAI/Topology/ArtinGroups/Complexes/HighConeIndex.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.highConeIndex line 14
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.highConeNormalized line 34
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.highConePivot line 38
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.highConeReduction line 50
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.highConeRetained_level line 57
6. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.highPureIndex line 64
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.highRestriction_top_eq_layer line 77