Theorems · Theorem · commutative algebra
IsLocalRing.of_singleton_maximalSpectrum
∀ {R : Type u_1} [inst : CommSemiring R] [Subsingleton (MaximalSpectrum R)] [Nonempty (MaximalSpectrum R)],
IsLocalRing RIf the maximal spectrum of a ring is a singleton, then the ring is local.
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites9
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
- Idealproof · cited by 4,748
- Ideal.IsMaximalproof · cited by 452
- IsLocalRingstatement · cited by 339
- Classical.arbitraryproof · cited by 161
- MaximalSpectrumstatement and proof · cited by 73
- MaximalSpectrum.asIdealproof · cited by 58
- IsLocalRing.of_unique_max_idealproof · cited by 4
- MaximalSpectrum.mk.injproof · cited by 2
Cited by2
Results whose statement or proof uses this declaration.
- PrimeSpectrum.subsingleton_iff_isField_of_isReducedproof · cited by 1
- IsLocalRing.not_isLocalRing_tfaeproof · cited by 1