Structures · Algebra
Ring.DimensionLEOne
A ring R has Krull dimension at most one if all nonzero prime ideals are maximal.
- Defined in
- Mathlib.RingTheory.DedekindDomain.Basic
- Shape
- One type argument · adds maximalOfPrime
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Concrete types that are instances1
- Subtype
How is a type an instance?
Loading the hierarchy index…
Assumed by11
- Ideal.IsPrime.isMaximal
- Ring.DimensionLEOne.maximalOfPrime
- Ring.DimensionLEOne.not_lt_lt
- Ring.DimensionLEOne.of_isIntegral
- Ring.DimensionLEOne.localization
- Ring.DimensionLeOne.prime_le_prime_iff_eq
- Ring.DimensionLEOne.isIntegralClosure
- Ring.DimensionLEOne.integralClosure
- Ring.DimensionLEOne.instKrullDimLEOfNatNat
- Ring.DimensionLEOne.eq_bot_of_lt
- Ring.DimensionLEOne.of_ringEquiv
Ancestors0
No ancestors.