Commit 2025-07-23 11:19 10d61c29

feat: Spec(R) notation for Spec (CommRingCat.of R) (#27031) This notation was instrumental in understanding the "industrial size" goals that showed up in Toric. Indeed, Spec (.of R) is reasonably short, but it currently pretty-prints as Spec (CommRingCat.of R), which is unbearably long. There is a slight potential for ambiguity with Spec R, which I have hopefully mitigated with a docstring. If ever someone nonetheless writes a lemma about Spec(R) where R : CommRingCat, all odds are that it will be innocuous since .of ↑R = R definitionally. Alternatively, we could make the Spec(R) notation and delaborator automatically detect whether R : CommRingCat or not. I would rather postpone this extra complexity until strictly necessary. From Toric