Theorems · Inductive type · commutative algebra
MaximalSpectrum
(R : Type u_1) → [CommSemiring R] → Type u_1
The maximal spectrum of a commutative (semi)ring R is the type of all
maximal ideals of R.
- Defined in
- Mathlib.RingTheory.Spectrum.Maximal.Defs
- Cited by
- 73 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement · cited by 10,911
Cited by95
Results whose statement or proof uses this declaration.
- MaximalSpectrum.asIdealstatement and proof · cited by 58
- MaximalSpectrum.PiLocalizationproof · cited by 17
- IsArtinianRing.equivPistatement · cited by 9
- MaximalSpectrum.toPiLocalizationstatement · cited by 9
- IsArtinianRing.primeSpectrumEquivMaximalSpectrumstatement and proof · cited by 7
- MaximalSpectrum.mapPiLocalizationstatement and proof · cited by 6
- MaximalSpectrum.toPrimeSpectrumstatement and proof · cited by 5
- PrimeSpectrum.piLocalizationToMaximalstatement and proof · cited by 3
- Algebra.FormallyEtale.equivPiOfIsSepClosedproof · cited by 3
- IsArtinianRing.nilradical_pow_eq_iInfstatement and proof · cited by 3
- MaximalSpectrum.iInf_localization_eq_botstatement and proof · cited by 3
- MaximalSpectrum.toPiLocalization_injectivestatement · cited by 3