OAI/Topology/ArtinGroups/Complexes/PlacedProjective.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.placedProjective line 12
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homSpace_zero_of_layer_gap line 20
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classHomDimension_zero_of_layer_gap line 35
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.bottom_last_row_zero line 43
5. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.placedGeneratorMap line 58
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.placedGenerator_homDimension_ne_zero line 74
7. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.classLowerBound_of_placed_vanishing line 94