OAI/Topology/ArtinGroups/Complexes/Shift.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.sourceShift line 15
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.sourceShift_pure line 32
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.sourceShift_cycle line 41
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.derivedMono_postcompose_injective line 59
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.derivedMono_coefficient_homDimension_mono line 87
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.derivedMono_total_coefficient_mono line 102
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.derivedSubobject_cartan_inequality line 117