mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard

refactor(algebraic_geometry/prime_spectrum/basic): refactor prime_spectrum def into structure

Open Multramate opened this issue 3 years ago • 1 comments
trafficstars

  • [x] depends on: #16920 [refactor height one spectrum]

Open in Gitpod

Multramate avatar Oct 12 '22 15:10 Multramate

This PR/issue depends on:

  • ~~leanprover-community/mathlib#16920~~ By Dependent Issues (🤖). Happy coding!

Canceled.

bors[bot] avatar Oct 25 '22 09:10 bors[bot]

@jcommelin could you tell bors to merge again?

Multramate avatar Oct 25 '22 16:10 Multramate

Please resolve the merge conflict. Thanks!

erdOne avatar Nov 06 '22 00:11 erdOne

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Nov 26 '22 14:11 bors[bot]