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: port Data.Real.CauSeqCompletion #1469
Conversation
This PR/issue depends on: |
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.
I really don't know why we had to revert #1440 over this, but it seems good to go now
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.
Thanks 🎉
bors merge
Unreverts #1440 Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded:
|
simp only [div_eq_mul_inv, ofRat_inv, ofRat_mul] | ||
#align cau_seq.completion.of_rat_div CauSeq.Completion.ofRat_div | ||
|
||
-- Porting note: removed |
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.
@Ruben-VandeVelde: why did you remove this?
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.
Because:
|
Unreverts #1440 Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
These files have been primarily modified by backports and need little modification: * `topology.basic`: #1826 - modified with a porting note, which can now be removed * `data.real.cau_seq_completion`: #1469 - not a backport, but forgot to update the SHA * `order.filter.n_ary.basic`: #1967 - this PR forgot to update the SHA * `ring_theory.valuation.basic`: The change is a small golf that is now included in this PR Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Unreverts #1440
parameters
mathlib#18122