Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(algebraic_geometry/Spec): (fβˆ— π’ͺβ‚›)β‚š is just the localization Sβ‚š for affine f : Spec S ⟢ Spec R #17471

Closed
erdOne wants to merge 1 commit into from
Closed

[Merged by Bors] - feat(algebraic_geometry/Spec): (fβˆ— π’ͺβ‚›)β‚š is just the localization Sβ‚š for affine f : Spec S ⟢ Spec R #17471

erdOne wants to merge 1 commit into from

Conversation

@erdOne
Copy link
Member

@erdOne erdOne commented Nov 11, 2022

Open in Gitpod

@erdOne erdOne added awaiting-review The author would like community review of the PR t-algebraic-geometry Algebraic geometry labels Nov 11, 2022
@erdOne erdOne requested a review from a team as a code owner November 11, 2022 07:29
jcommelin
jcommelin approved these changes Dec 7, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks πŸŽ‰

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Dec 7, 2022
bors bot pushed a commit that referenced this pull request Dec 7, 2022
@erdOne
feat(algebraic_geometry/Spec): (fβˆ— π’ͺβ‚›)β‚š is just the localization `S…
4f785b6 
β€¦β‚š` for affine `f : Spec S ⟢ Spec R` (#17471)
@bors
Copy link

bors bot commented Dec 7, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebraic_geometry/Spec): (fβˆ— π’ͺβ‚›)β‚š is just the localization Sβ‚š for affine f : Spec S ⟢ Spec R [Merged by Bors] - feat(algebraic_geometry/Spec): (fβˆ— π’ͺβ‚›)β‚š is just the localization Sβ‚š for affine f : Spec S ⟢ Spec R Dec 7, 2022
@bors bors bot closed this Dec 7, 2022
@bors bors bot deleted the to_pushforward_stalk branch December 7, 2022 10:41
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

1 more reviewer

@jcommelin jcommelin jcommelin approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-algebraic-geometry Algebraic geometry

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@erdOne @jcommelin @leanprover-community-bot-assistant