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(ring_theory/etale): Localization and formally etale homomorphisms. #15813
Conversation
erdOne
commented
Aug 2, 2022
src/ring_theory/etale.lean
Outdated
/-- This actually does not need the localization instance, and is stated here again for | ||
consistency. See `algebra.formally_unramified.of_comp` instead. -/ | ||
@[nolint unused_arguments] |
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.
Can't you use an alias
and avoid the unused_arguments
?
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.
This is here so that one would not need to change anything (including removing redundant arguments) when copying proofs for formally_{unramified, smooth, etale}
.
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.
bors d+
✌️ erdOne can now approve this pull request. To approve and merge a pull request, simply reply with |
Co-authored-by: Johan Commelin <johan@commelin.net>
bors r+ |
…s. (#15813) Co-authored-by: Andrew Yang <36414270+erdOne@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |