OAI/NumberTheory/PiExponent/Polynomials/GradedLocalizationFree.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.GradedLocalizationFree.coordinateMap line 14
2. theorem OAI.PiExponent.GradedLocalizationFree.coordinateMap_fraction line 20
3. theorem OAI.PiExponent.GradedLocalizationFree.coordinateMap_injective line 25
4. def OAI.PiExponent.GradedLocalizationFree.coordinatePieces line 59
5. theorem OAI.PiExponent.GradedLocalizationFree.coordinatePieces_coe line 77
6. theorem OAI.PiExponent.GradedLocalizationFree.coordinatePieces_injective line 81
7. theorem OAI.PiExponent.GradedLocalizationFree.coordinatePieces_surjective line 88
8. def OAI.PiExponent.GradedLocalizationFree.shiftedFreeEquiv line 116
9. theorem OAI.PiExponent.GradedLocalizationFree.shiftedFreeEquiv_apply line 123