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

golfed imports

Browse source
This commit is contained in:
leopoldmayer 2023-06-16 09:54:07 -07:00
parent bcb867258a
commit d0a6d8605e
1 changed files with 0 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
CommAlg/polynomial.lean
View file

@ -1,13 +1,3 @@
import Mathlib.RingTheory.Ideal.Operations
import Mathlib.RingTheory.FiniteType
import Mathlib.Order.Height
import Mathlib.RingTheory.Polynomial.Quotient
import Mathlib.RingTheory.PrincipalIdealDomain
import Mathlib.RingTheory.DedekindDomain.Basic
import Mathlib.RingTheory.Ideal.Quotient
import Mathlib.RingTheory.Localization.AtPrime
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
import Mathlib.Order.ConditionallyCompleteLattice.Basic
import CommAlg.krull import CommAlg.krull
section ChainLemma section ChainLemma
@ -132,7 +122,6 @@ lemma ht_adjoin_x_eq_ht_add_one [Nontrivial R] (I : PrimeSpectrum R) : height I
apply hl.2 apply hl.2
exact hb exact hb
#check (⊤ : ℕ∞)
/- /-
dim R + 1 ≤ dim R[X] dim R + 1 ≤ dim R[X]
-/ -/