SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-10-16 11:37:05 -05:00
Code Issues Projects Releases Packages Wiki Activity

added more references to readme

Browse source
This commit is contained in:
GTBarkley 2023-06-10 18:40:48 -04:00 committed by GitHub
parent 59a056f82f
commit 9a08a59274
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
README.md
View file

@ -9,6 +9,8 @@ Feel free to add, modify, and expand this file. Below are starting points for th
- Definitions of an ideal, prime ideal, and maximal ideal:
```lean
def Mathlib.RingTheory.Ideal.Basic.Ideal (R : Type u) [Semiring R] := Submodule R R
class Mathlib.RingTheory.Ideal.Basic.IsPrime (I : Ideal α) : Prop
class IsMaximal (I : Ideal α) : Prop
```
- Definition of a Spec of a ring: `Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic.PrimeSpectrum`
@ -31,7 +33,7 @@ Give Examples of each of the above cases for a particular instances of ring
Theorem 0: Hilbert Basis Theorem:
```lean
instance isNoetherianRing [Finite σ] [IsNoetherianRing R] : IsNoetherianRing (MvPolynomial σ R)
theorem Mathlib.RingTheory.Polynomial.Basic.Polynomial.isNoetherianRing [inst : IsNoetherianRing R] : IsNoetherianRing R[X]
```
Theorem 1: If A is a nonzero ring, then dim A[t] >= dim A +1