Adam Topaz

To be honest, this notation looks quite awkward. And since it's not too similar (unless you really squint) to what we would write on paper, I'm not sure if it's...

One potential solution is to add tags to mathlib4 associated to the relevant versions, and add mathlib4 as a dependency pointing to the specific tag. That would push some responsibility...

I guess one question we need to answer is who the intended audience for these files actually is. My original intention was for these to be read by mathematicians who...

There is quite a lot going on in this PR. I see at least four contributions: 1. `GlueData'` 2. Disjoint unions of schemes. 3. Disjoint unions of prime spectra. 4....