OAI/NumberTheory/PiExponent/Ampleness/ReesGradedModule.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.PiExponent.ReesGradedModule.integerPiece line 14
2. instance OAI.PiExponent.ReesGradedModule.integerGradedRing line 17
3. def OAI.PiExponent.ReesGradedModule.ordinaryPowerEquivIntegerPiece line 21
4. theorem OAI.PiExponent.ReesGradedModule.polynomial_negative_eq_zero line 24
5. theorem OAI.PiExponent.ReesGradedModule.presentation_integer_mem line 33
6. def OAI.PiExponent.ReesGradedModule.gradedPresentation line 47
7. theorem OAI.PiExponent.ReesGradedModule.presentation_degree_compatible line 51
8. theorem OAI.PiExponent.ReesGradedModule.gradedScalarAction line 56
9. theorem OAI.PiExponent.ReesGradedModule.finite_graded_module line 65