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] - refactor(analysis/asymptotics): make definitions immediately irreducible #6021
Conversation
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+
src/analysis/asymptotics.lean
Outdated
@@ -383,12 +403,12 @@ by simp only [is_O_with, norm_norm] | |||
alias is_O_with_norm_right ↔ asymptotics.is_O_with.of_norm_right asymptotics.is_O_with.norm_right | |||
|
|||
@[simp] theorem is_O_norm_right : is_O f (λ x, ∥g' x∥) l ↔ is_O f g' l := | |||
exists_congr $ λ _, is_O_with_norm_right | |||
by unfold is_O; exact exists_congr (λ _, is_O_with_norm_right) |
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.
by unfold is_O; exact exists_congr (λ _, is_O_with_norm_right) | |
by { unfold is_O, exact exists_congr (λ _, is_O_with_norm_right) } |
Here and below, can you use the by { t1, t2 }
idiom instead of by t1; t2
?
✌️ gebner can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
Pull request successfully merged into master. Build succeeded: |
In preparation of 🍀, where
attribute [irreducible]
will no longer work.