OAI/Topology/ArtinGroups/Complexes/TermwiseSplitInjection.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.TermwiseSplitInjection line 13
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.postcomposeOnCycles line 19
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.postcomposeOnCycles_injective line 29
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.pure_coefficient_homDimension_mono line 46
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.totalHomDimension_eq_sum_of_subset line 59
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.pure_total_coefficient_homDimension_mono line 69
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.subobject_cartan_inequality line 83