mirror of
https://github.com/GTBarkley/comm_alg.git
synced 2025-04-07 22:08:03 -05:00
15 lines
391 B
Text
15 lines
391 B
Text
import Mathlib.RingTheory.Ideal.Basic
|
|
import Mathlib.RingTheory.Noetherian
|
|
import Mathlib.RingTheory.Artinian
|
|
import Mathlib.RingTheory.Ideal.Quotient
|
|
import Mathlib.AlgebraicGeometry.PrimeSpectrum.Basic
|
|
|
|
lemma dim_zero_Noetherian_is_Artinian (R : Type _) (IsNoetherianRing R) (krull_dim R = 0) : IsArtinianRing R := by sorry
|
|
|
|
-- Use Stacks project proof since it's broken into lemmas
|
|
|
|
|
|
|
|
|
|
|
|
|