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] - chore: re-port Algebra.CharP.Basic #3191
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+
Thanks!
✌️ joneugster can now approve this pull request. To approve and merge a pull request, simply reply with |
Thx Jeremy for fixing the newline + bors r+ |
This forward-ports changes from leanprover-community/mathlib#11364 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
This forward-ports changes from leanprover-community/mathlib#11364 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
bors merge |
This forward-ports changes from leanprover-community/mathlib#11364 Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Build failed: |
Can you merge master? |
bors merge |
This forward-ports changes from leanprover-community/mathlib#11364 One unrelated downstream file times out, presumably due to the import graph subtly changing. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded:
|
This forward-ports changes from leanprover-community/mathlib#11364 One unrelated downstream file times out, presumably due to the import graph subtly changing. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This forward-ports changes from leanprover-community/mathlib#11364 One unrelated downstream file times out, presumably due to the import graph subtly changing. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This forward-ports changes from leanprover-community/mathlib#11364
One unrelated downstream file times out, presumably due to the import graph subtly changing.
algebra.char_p.basic
@05a78c9451101108e638a0f213fb1bed82483545
..ceb887ddf3344dab425292e497fa2af91498437c
This is the last file from mathlib#11364. The other files are: