Theorems · Definition · commutative algebra
MaximalSpectrum.asIdeal
{R : Type u_1} → [inst : CommSemiring R] → MaximalSpectrum R → Ideal R- Defined in
- Mathlib.RingTheory.Spectrum.Maximal.Defs
- Cited by
- 58 results in Mathlib
- Foundations
- Depth 15 from the axioms · uses no axioms
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
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
- Idealstatement · cited by 4,748
- MaximalSpectrumstatement and proof · cited by 73
Cited by73
Results whose statement or proof uses this declaration.
- MaximalSpectrum.PiLocalizationproof · cited by 17
- IsArtinianRing.equivPistatement · cited by 9
- MaximalSpectrum.toPiLocalizationstatement · cited by 9
- IsArtinianRing.primeSpectrumEquivMaximalSpectrumproof · cited by 7
- MaximalSpectrum.mapPiLocalizationstatement and proof · cited by 6
- MaximalSpectrum.toPrimeSpectrumproof · cited by 5
- PrimeSpectrum.piLocalizationToMaximalstatement · 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 and proof · cited by 3
- PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalizationstatement · cited by 2