OAI/NumberTheory/PiExponent/Polynomials/ShiftedFreeGrading.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.ShiftedFreeGrading.piece line 13
2. def OAI.PiExponent.ShiftedFreeGrading.component line 19
3. def OAI.PiExponent.ShiftedFreeGrading.support line 23
4. theorem OAI.PiExponent.ShiftedFreeGrading.component_eq_zero_of_not_mem line 28
5. def OAI.PiExponent.ShiftedFreeGrading.decompositionMap line 42
6. theorem OAI.PiExponent.ShiftedFreeGrading.decompositionMap_apply line 62
7. theorem OAI.PiExponent.ShiftedFreeGrading.decompositionMap_injective line 66
8. theorem OAI.PiExponent.ShiftedFreeGrading.decompositionMap_homogeneous line 77
9. instance OAI.PiExponent.ShiftedFreeGrading.decomposition line 89
10. theorem OAI.PiExponent.ShiftedFreeGrading.decompose_apply line 103