SinTan1729/comm_alg
1
0
Fork 0
mirror of https://github.com/GTBarkley/comm_alg.git synced 2024-12-26 23:48:36 -06:00
Code Issues Projects Releases Packages Wiki Activity

Merge pull request #9 from GTBarkley/grant

Browse source 
added more references to mathlib to readme
This commit is contained in:
GTBarkley 2023-06-10 15:54:44 -07:00 committed by GitHub
commit d28fcc1b57
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 9 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
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: - Definitions of an ideal, prime ideal, and maximal ideal:
```lean ```lean
def Mathlib.RingTheory.Ideal.Basic.Ideal (R : Type u) [Semiring R] := Submodule R R 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` - Definition of a Spec of a ring: `Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic.PrimeSpectrum`
@ -16,9 +18,14 @@ def Mathlib.RingTheory.Ideal.Basic.Ideal (R : Type u) [Semiring R] := Submodule
- Definition of a Noetherian and Artinian rings: - Definition of a Noetherian and Artinian rings:
```lean ```lean
class Mathlib.RingTheory.Noetherian.IsNoetherian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop class Mathlib.RingTheory.Noetherian.IsNoetherian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop
class Mathlib.RingTheory.Artinian.IsArtinian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop
``` ```
- Definition of a polynomial ring: `Mathlib.RingTheory.Polynomial.Basic`
- Definitions of a local ring and quotient ring - Definitions of a local ring and quotient ring: `Mathlib.RingTheory.Ideal.Quotient.?`
```lean
class Mathlib.RingTheory.Ideal.LocalRing.LocalRing (R : Type u) [Semiring R] extends Nontrivial R : Prop
```
- Definition of the chain of prime ideals and the length of these chains - Definition of the chain of prime ideals and the length of these chains
@ -31,7 +38,7 @@ Give Examples of each of the above cases for a particular instances of ring
Theorem 0: Hilbert Basis Theorem: Theorem 0: Hilbert Basis Theorem:
```lean ```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 Theorem 1: If A is a nonzero ring, then dim A[t] >= dim A +1