OAI/Algebra/AffineCancellation/ModificationGrading.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ComplexCancellation.AffineModification.weight line 11
2. def OAI.ComplexCancellation.AffineModification.sourcePieces line 12
3. instance OAI.ComplexCancellation.AffineModification.sourceGrading line 13
4. lemma OAI.ComplexCancellation.AffineModification.rel_homogeneous line 15
5. lemma OAI.ComplexCancellation.AffineModification.kernel_homogeneous line 20
6. def OAI.ComplexCancellation.AffineModification.pieces line 28
7. instance OAI.ComplexCancellation.AffineModification.grading line 29
8. lemma OAI.ComplexCancellation.AffineModification.monomial_image line 31
9. lemma OAI.ComplexCancellation.AffineModification.weight_eq line 40
10. lemma OAI.ComplexCancellation.AffineModification.monomial_reduction line 47
11. lemma OAI.ComplexCancellation.AffineModification.piece_negative line 51
12. lemma OAI.ComplexCancellation.AffineModification.piece_even line 68
13. lemma OAI.ComplexCancellation.AffineModification.piece_odd line 87
14. lemma OAI.ComplexCancellation.AffineModification.degree_cases line 106
15. lemma OAI.ComplexCancellation.AffineModification.piece_monomial line 113
16. lemma OAI.ComplexCancellation.AffineModification.V_dvd_of_positive line 126
17. lemma OAI.ComplexCancellation.AffineModification.degree_even_of_not_τ_dvd line 137
18. lemma OAI.ComplexCancellation.AffineModification.coefficient_mem line 152
19. lemma OAI.ComplexCancellation.AffineModification.τ_mem line 154
20. lemma OAI.ComplexCancellation.AffineModification.V_mem line 155