Theorems · Theorem · ring theory
IsNoetherianRing.isArtinianRing_of_krullDimLE_zero
∀ {R : Type u_3} [inst : CommRing R] [IsNoetherianRing R] [Ring.KrullDimLE 0 R], IsArtinianRing R- Defined in
- Mathlib.RingTheory.HopkinsLevitzki
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites30
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setproof · cited by 53,352
- CommRingstatement and proof · cited by 17,173
- Fieldproof · cited by 7,404
- Set.Elemproof · cited by 7,166
- Set.ofPredproof · cited by 6,101
- Idealproof · cited by 4,748
- Finiteproof · cited by 3,029
- HasQuotient.Quotientproof · cited by 2,301
- Ideal.IsPrimeproof · cited by 827
- RingEquiv.symmproof · cited by 567
- Set.Finite.subsetproof · cited by 285
- IsNoetherianRingstatement and proof · cited by 268
Cited by2
Results whose statement or proof uses this declaration.
- isArtinianRing_iff_isNoetherianRing_krullDimLE_zeroproof · cited by 3
- IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRingproof · cited by 1