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

adjusted height definition

Browse source
This commit is contained in:
GTBarkley 2023-06-12 04:15:30 +00:00
parent 1f6dd08dd4
commit 6528571d32
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
comm_alg/krull.lean
View file

@ -20,7 +20,7 @@ namespace Ideal
variable {R : Type _} [CommRing R] (I : PrimeSpectrum R) variable {R : Type _} [CommRing R] (I : PrimeSpectrum R)
noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J ≤ I} - 1 noncomputable def height : ℕ∞ := Set.chainHeight {J : PrimeSpectrum R | J < I}
noncomputable def krull_dim (R : Type) [CommRing R]: WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I noncomputable def krull_dim (R : Type) [CommRing R]: WithBot ℕ∞ := ⨆ (I : PrimeSpectrum R), height I