OAI/Topology/ArtinGroups/Complexes/CoefficientSocle.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.coefficientSocle line 12
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.entry_vertex_left_support line 32
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.entry_vertex_right_support line 41
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.coefficient_row_zero line 50
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.coefficient_cocycle_zero_of_socle_zero line 65
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.pure_coefficient_homDimension_zero_of_socle_zero line 124
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.pure_total_coefficient_homDimension_zero_of_socle_zero line 142
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.coefficientSocle_nonzero_at_max line 157
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.exists_coefficientSocle_nonzero line 180