Theorems · Inductive type · commutative algebra
Ideal.FiniteHeight
{R : Type u_1} → [inst : CommRing R] → Ideal R → PropAn 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
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses no axioms
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by20
Results whose statement or proof uses this declaration.
- Ideal.height_ne_topstatement and proof · cited by 5
- Ideal.height_lt_topstatement and proof · cited by 4
- Ideal.height_strict_mono_of_isPrimestatement and proof · cited by 4
- Ideal.mem_minimalPrimes_of_height_lestatement and proof · cited by 3
- Ideal.finiteHeight_iffstatement and proof · cited by 3
- Ideal.height_strict_mono_of_isPrime_of_isPrimestatement and proof · cited by 3
- Ideal.eq_span_singleton_of_height_eq_oneproof · cited by 2
- Ideal.exists_ltSeries_length_eq_heightstatement and proof · cited by 1
- exists_spanRank_le_and_le_height_of_le_heightproof · cited by 1
- Ideal.FiniteHeight.casesOnstatement and proof · cited by 1
- Ideal.FiniteHeight.eq_top_or_height_ne_topstatement and proof · cited by 1
- Ideal.mem_minimalPrimes_span_of_mem_minimalPrimes_span_insertproof · cited by 1