mathlib icon indicating copy to clipboard operation
mathlib copied to clipboard
verified publisher icon leanprover-community

refactor(algebraic_geometry/projective_spectrum/topology): refactor projective_spectrum def into structure

Open Multramate opened this issue 3 years ago • 1 comments

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

Open in Gitpod

Multramate avatar Oct 12 '22 15:10 Multramate

This PR/issue depends on:

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

mathlib-dependent-issues-bot avatar Oct 12 '22 17:10 mathlib-dependent-issues-bot

This PR/issue depends on:

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

mathlib-dependent-issues-bot avatar Nov 26 '22 15:11 mathlib-dependent-issues-bot

Pull request successfully merged into master.

Build succeeded:

bors[bot] avatar Dec 07 '22 15:12 bors[bot]