OAI/Topology/ArtinGroups/Quivers/CotestPlacement.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.cotestPlacement line 12
2. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.cotestMatrix_degree line 16
3. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.coevaluationMatrix line 29
4. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.coevaluation_entries line 34
5. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.coevaluation_degree line 51
6. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.mul_coevaluation line 73
7. lemma OAI.HarmonicArtin.ReversibleQuiver.Zigzag.coevaluation_testMatrix line 83
8. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.cotestComplex line 111
9. def OAI.HarmonicArtin.ReversibleQuiver.Zigzag.BasedComplex.coevaluation line 121