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

feat(algebraic_geometry/projective_spectrum/scheme): add an equivalent definition of `from_Spec.carrier`

Open jjaassoonn opened this issue 3 years ago • 2 comments

This is definition "computes better", so it is needed when showing from_Spec and to_Spec are inverses

  • [x] depends on: #16693

Open in Gitpod

jjaassoonn avatar Sep 30 '22 22:09 jjaassoonn

This PR/issue depends on:

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

mathlib-dependent-issues-bot avatar Oct 05 '22 21:10 mathlib-dependent-issues-bot

Also, is it clear that we need both definitions? Or can we just use the new one everywhere?

jcommelin avatar Oct 13 '22 06:10 jcommelin