mathlib
mathlib copied to clipboard
refactor(algebraic_geometry/prime_spectrum/basic): refactor prime_spectrum def into structure
This PR/issue depends on:
- ~~leanprover-community/mathlib#16920~~ By Dependent Issues (🤖). Happy coding!
Canceled.
@jcommelin could you tell bors to merge again?
Please resolve the merge conflict. Thanks!
Pull request successfully merged into master.
Build succeeded: