Commit 2024-02-21 19:00 8eef2a77

feat: add a SpectrumRestricts structure (#10735) when A is and S-algebra and R is a subring of S, SpectrumRestricts (a : A) (f : S → R) means that the S-spectrum of a is entirely contained within the image of the R-spectrum of a under algebraMap R S. We include f because we want to explicitly specify the function that takes us back into R from S.