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 #10 from GTBarkley/Jayden

Browse source 
Jayden
This commit is contained in:
GTBarkley 2023-06-10 16:32:40 -07:00 committed by GitHub
commit f89eaefb89
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
CommAlg.lean
View file

@ -1 +1,4 @@
def hello := "world" import Mathlib.Tactic
def hello := "world"
-- Thank Grant for setting this up.

4
README.md
View file

@ -31,6 +31,8 @@ class Mathlib.RingTheory.Ideal.LocalRing.LocalRing (R : Type u) [Semiring R] ext
- Definition of the Krull dimension (supremum of the lengh of chain of prime ideal): `Mathlib.Order.KrullDimension.krullDim` - Definition of the Krull dimension (supremum of the lengh of chain of prime ideal): `Mathlib.Order.KrullDimension.krullDim`
- Krull dimension of a module
- 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): `Mathlib.Order.KrullDimension.height`
@ -47,4 +49,6 @@ 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 Theorem 3: If A is nonzero ring then dim A_p + dim A/p <= dim A
Lemma 0: A ring is artinian iff it is noetherian of dimension 0.
Definition of a graded module Definition of a graded module