OAI/Algebra/AffineCancellation/QuotientGrading.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ComplexCancellation.QuotientGrading.pieces line 14
2. def OAI.ComplexCancellation.QuotientGrading.componentMap line 16
3. def OAI.ComplexCancellation.QuotientGrading.sourceDecompose line 19
4. lemma OAI.ComplexCancellation.QuotientGrading.sourceDecompose_apply line 22
5. lemma OAI.ComplexCancellation.QuotientGrading.sourceDecompose_zero line 25
6. lemma OAI.ComplexCancellation.QuotientGrading.sourceDecompose_eq line 31
7. def OAI.ComplexCancellation.QuotientGrading.decomposeMap line 41
8. lemma OAI.ComplexCancellation.QuotientGrading.decomposeMap_q line 55
9. lemma OAI.ComplexCancellation.QuotientGrading.coe_sourceDecompose line 60
10. lemma OAI.ComplexCancellation.QuotientGrading.decomposeMap_homogeneous line 74
11. def OAI.ComplexCancellation.QuotientGrading.decomposition line 85
12. def OAI.ComplexCancellation.QuotientGrading.grading line 103
13. lemma OAI.ComplexCancellation.QuotientGrading.projection_q line 113