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 #12 from GTBarkley/grant

Browse source 
checked preliminary definition of Krull dimension
This commit is contained in:
GTBarkley 2023-06-10 17:37:21 -07:00 committed by GitHub
commit d1c10a2d3a
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 8 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
comm_alg/grant.lean
View file

@ -1,6 +1,12 @@
import Mathlib.Analysis.Seminorm
import Mathlib.Order.KrullDimension
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
def hello : IO Unit := do
IO.println "Hello, World!"
#eval hello
#check (p q : PrimeSpectrum _) → (p ≤ q)
#check Preorder (PrimeSpectrum _)
#check krullDim (PrimeSpectrum _)