FMLJohn
FMLJohn
I have proved that for a Noetherian graded ring, its 0th grade is also a Noetherian ring.
@kbuzzard @eric-wieser
> What happened with the idea of having a predicate `krullDimLT` that asserted that the krullDim of a given ring/space/... was LT a given natural number? Is there a discussion...
> Also please use `variable {R S : Type*} [CommRing R] [CommRing S]` at the top of the file. Done!
> I think Johan is referring to @kbuzzard's idea that instead of defining `krullDim`, we can introduce a family of predicate `krullDimLT`, then the negative infinity case is `krullDimLT 0`,...
I have added a file HilbertPolynomial.lean to the folder Mathlib/Algebra/HilbertSerre. In the file, the main things I have done are: 1. formalising the Hilbert polynomial (`HilbertSerre.hilbertPolynomial`), which is a one-variable...