Commit 2025-08-18 09:17 cc8626ea
View on Github →feat(RingTheory/Spectrum/Prime): f : R →+* S is local if the induced map Spec S → Spec R is surjective (#28121)
f : R →+* S is local if the induced map Spec S → Spec R is surjective.
feat(RingTheory/Spectrum/Prime): f : R →+* S is local if the induced map Spec S → Spec R is surjective (#28121)
f : R →+* S is local if the induced map Spec S → Spec R is surjective.