Theorems · Theorem · algebraic geometry
PrimeSpectrum.finite_setOfPred_isMin
∀ (R : Type u) [inst : CommSemiring R] [IsNoetherianRing R], {x | IsMin x}.Finite- Cited by
- 2 results in Mathlib
- Foundations
- Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiringIsNoetherianRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites15
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Set.ofPredstatement and proof · cited by 6,101
- Set.imageproof · cited by 5,609
- Set.Finitestatement and proof · cited by 1,814
- PrimeSpectrumstatement and proof · cited by 625
- PrimeSpectrum.asIdealproof · cited by 333
- Set.Finite.subsetproof · cited by 285
- Function.Injective.injOnproof · cited by 280
- IsMinstatement · cited by 277
- IsNoetherianRingstatement and proof · cited by 268
- Set.image_preimage_subsetproof · cited by 75
- PrimeSpectrum.extproof · cited by 43
Cited by2
Results whose statement or proof uses this declaration.
- PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRingproof · cited by 2
- PrimeSpectrum.finite_setOf_isMinproof · cited by 0