Commit 2024-05-21 11:01 c187e36a
View on Github →chore(AlgebraicGeometry): minor cleanup (#13080)
Motivated by trying to clean up CommRingCat and friends, but this is a downstream fix that seems fine independently (and helpful later).
chore(AlgebraicGeometry): minor cleanup (#13080)
Motivated by trying to clean up CommRingCat and friends, but this is a downstream fix that seems fine independently (and helpful later).