[Merged by Bors] - refactor(AlgebraicGeometry): Introduce Scheme.Opens.#15001
Closed
erdOne wants to merge 24 commits intomasterfrom erd1/schemeOpens2
Commits
Commits on Jul 22, 2024
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
- committed
Commits on Jul 23, 2024
Merge branch 'master' of https://github.com/leanprover-community/mathlib4 into erd1/schemeOpens2
committed- committed
- committed
- committed
- committed
