OAI/NumberTheory/PiExponent/Polynomials/NatToIntGrading.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.NatToIntGrading.piece line 11
2. def OAI.PiExponent.NatToIntGrading.component line 15
3. def OAI.PiExponent.NatToIntGrading.support line 19
4. theorem OAI.PiExponent.NatToIntGrading.component_eq_zero_of_not_mem line 23
5. def OAI.PiExponent.NatToIntGrading.decompositionMap line 37
6. theorem OAI.PiExponent.NatToIntGrading.decompositionMap_nat line 66
7. theorem OAI.PiExponent.NatToIntGrading.decompositionMap_injective line 69
8. theorem OAI.PiExponent.NatToIntGrading.decompositionMap_homogeneous line 75
9. instance OAI.PiExponent.NatToIntGrading.decomposition line 100
10. theorem OAI.PiExponent.NatToIntGrading.decompose_nat line 112
11. theorem OAI.PiExponent.NatToIntGrading.decompose_negSucc line 115
12. instance OAI.PiExponent.NatToIntGrading.gradedSMul line 122
13. instance OAI.PiExponent.NatToIntGrading.gradedMonoid line 145