OAI/Algebra/AffineCancellation/ReesGrading.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ComplexCancellation.Rees.weight line 12
2. def OAI.ComplexCancellation.Rees.sourcePieces line 13
3. instance OAI.ComplexCancellation.Rees.sourceGrading line 14
4. lemma OAI.ComplexCancellation.Rees.xp_homogeneous line 15
5. lemma OAI.ComplexCancellation.Rees.relation_homogeneous line 26
6. lemma OAI.ComplexCancellation.Rees.kernel_homogeneous line 44
7. def OAI.ComplexCancellation.Rees.pieces line 51
8. instance OAI.ComplexCancellation.Rees.grading line 52
9. abbrev OAI.ComplexCancellation.Rees.laurentPieces line 53
10. instance OAI.ComplexCancellation.Rees.laurentGrading line 54
11. lemma OAI.ComplexCancellation.Rees.laurentMonomial_mem line 55
12. lemma OAI.ComplexCancellation.Rees.embedding_graded line 58
13. lemma OAI.ComplexCancellation.Rees.red_graded line 77
14. lemma OAI.ComplexCancellation.Rees.red_monomial_mem line 90