3a45dc52d7
First draft of the Readme file. It is just a list of things to do but need to be more descriptive. |
||
|---|---|---|
| .docker/gitpod | ||
| comm_alg | ||
| .gitignore | ||
| CommAlg.lean | ||
| gitpod.yml | ||
| lake-manifest.json | ||
| lakefile.lean | ||
| lean-toolchain | ||
| README.md | ||
| Readme.md | ||
comm_alg
SLMath collaboration for adding Krull dimension and Hilbert polynomial to mathlib
We start the comm algebra project by important definitions and theorems and go from there. Feel free to add, modify, and expand this file. Below are starting point for the project:
Definitions of an ideal, prime ideal, and maximal ideal Definition of a Spec of a ring Definition of a Noetherian and Artinian rings Definition of a local ring and quotient ring Definition of the Krull dimension
Give examples of each of the above cases for a particular instances of ring
Theorem 0: Hilbert Basis Theorem Theorem 1: If A is a nonzero ring, then dim A[t] >= dim A +1 Theorem 2: If A is a nonzero noetherian ring, then dim A[t] = dim A + 1 Theorem 3: If A is nonzero ring then dim A_p + dim A/p <= dim A