Structures · Algebra
Ideal.FiniteHeight
An ideal has finite height if it is either the unit ideal or its height is finite.
We include the unit ideal in order to have the instance IsNoetherianRing R → FiniteHeight I.
- Defined in
- Mathlib.RingTheory.Ideal.Height
- Shape
- One type argument · adds eq_top_or_height_ne_top
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by13
- Ideal.height_ne_top
- Ideal.height_lt_top
- Ideal.height_strict_mono_of_isPrime
- Ideal.height_strict_mono_of_isPrime_of_isPrime
- Ideal.mem_minimalPrimes_of_height_le
- Ideal.FiniteHeight.eq_top_or_height_ne_top
- Ideal.exists_ltSeries_length_eq_height
- Ideal.finiteHeight_of_le
- Ideal.height_lt_top_of_isPrime
- Ideal.height_ne_top_of_isPrime
- Ideal.height_strict_mono_of_isPrime_of_is_prime
- Ideal.mem_minimalPrimes_of_height_eq
- Ideal.eq_of_le_of_height_le
Ancestors0
No ancestors.