OAI/Topology/ArtinGroups/Complexes/ScalarKernel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarKernel line 14
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.PlacementSupported line 17
3. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.differential_arrow_right_support line 21
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.coefficientOutgoing line 27
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.coefficientOutgoing_support line 31
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarKernel.outgoing line 45
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.ScalarKernel.project line 84
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.scalarKernel_has_socle line 112
9. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.pureMap_scalarKernel_zero line 157
10. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.Map.scalarMatrix line 202
11. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.map_vertex_source_eq_target line 206
12. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.map_coefficient_entry line 215
13. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.scalarKernel_of_vecMul_zero line 231
14. theorem OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.pureMap_termwiseSplit line 242