OAI/NumberTheory/PiExponent/Ampleness/ReesPolynomialPresentation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PiExponent.ReesPolynomialPresentation.presentation line 12
2. theorem OAI.PiExponent.ReesPolynomialPresentation.presentation_X line 15
3. theorem OAI.PiExponent.ReesPolynomialPresentation.presentation_monomial_mem line 18
4. theorem OAI.PiExponent.ReesPolynomialPresentation.presentation_homogeneous_mem line 32
5. theorem OAI.PiExponent.ReesPolynomialPresentation.evaluation_presentation line 42
6. theorem OAI.PiExponent.ReesPolynomialPresentation.homogeneous_piece_surjective line 53
7. theorem OAI.PiExponent.ReesPolynomialPresentation.presentation_surjective line 74
8. def OAI.PiExponent.ReesPolynomialPresentation.presentationAlgebra line 91
9. theorem OAI.PiExponent.ReesPolynomialPresentation.finite_presented_module line 94
10. theorem OAI.PiExponent.ReesPolynomialPresentation.exists_finite_presentation line 102