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

add more mathlib refs to readme

Browse source
This commit is contained in:
GTBarkley 2023-06-10 18:19:33 -04:00 committed by GitHub
parent 73a1edf070
commit c95b28d69c
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 12 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
README.md
View file

@ -11,21 +11,28 @@ Feel free to add, modify, and expand this file. Below are starting points for th
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
``` ```
- Definition of a Spec of a ring - Definition of a Spec of a ring: `Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic.PrimeSpectrum`
- Definition of a Noetherian and Artinian rings - Definition of a Noetherian and Artinian rings:
```lean
class Mathlib.RingTheory.Noetherian.IsNoetherian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop
```
- Definitions of a local ring and quotient ring - Definitions of a local ring and quotient ring
- 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
- Definition of the Krull dimension (supremum of the lengh of chain of prime ideal) - Definition of the Krull dimension (supremum of the lengh of chain of prime ideal): `Mathlib.Order.KrullDimension.krullDim`
- Definition of the height of prime ideal (dimension of A_p): `Mathlib.Order.KrullDimension.height`
- Definition of the height of prime ideal (dimension of A_p)
Give Examples of each of the above cases for a particular instances of ring 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
instance isNoetherianRing [Finite σ] [IsNoetherianRing R] : IsNoetherianRing (MvPolynomial σ R)
```
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