-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(algebraic_geometry): Restriction of morphisms onto open sets of the target #14972
Conversation
erdOne
commented
Jun 26, 2022
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Looks good!
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
…munity/mathlib into morphism_restrict
I made some formatting edits in a new branch. Mainly, I wouldn't indent after an equal sign or ≅, for example here, but others might have different opinion? Another change is in affine_basis_cover_is_basis whose statement is made more succinct. |
Thanks! |
Actually a recent commit by a maintainer does use indentation after =, so there's definite a different opinion, so feel free to revert those changes. |
Thanks 🎉 bors merge |
…the target (#14972) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Build failed (retrying...): |
…the target (#14972) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
…the target (#14972) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>