OAI/Topology/ArtinGroups/Quivers/TraceLinear.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.trace_smul line 11
2. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.traceLinear line 14
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homCycles line 22
4. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homBoundaries line 26
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homBoundaries_le_homCycles line 31
6. abbrev OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.homCohomology line 43
7. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.supertrace line 48
8. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.supertrace_mul line 59
9. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.supertrace_boundary line 81