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(algebra/associated): split off dependencies of big_operators
#10848
Conversation
This prepares for the replacement of `nat.prime` with `_root_.prime` by reducing the amount of dependencies needed to define `_root_.prime`. Note that there wouldn't be an import loop without this change, just that `data/nat/prime.lean` would have a bigger amount of imports. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/nat.2Eprime
✌️ Vierkantor can now approve this pull request. To approve and merge a pull request, simply reply with |
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+
(assuming no further changes beyond adding import
lines
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
👎 Rejected by label |
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
bors merge |
…10848) This prepares for the replacement of `nat.prime` with `_root_.prime` by reducing the amount of dependencies needed to define `_root_.prime`. Note that there wouldn't be an import loop without this change, just that `data/nat/prime.lean` would have a bigger amount of imports. Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/nat.2Eprime Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded: |
big_operators
big_operators
This prepares for the replacement of
nat.prime
with_root_.prime
by reducing the amount of dependencies needed to define_root_.prime
.Note that there wouldn't be an import loop without this change, just that
data/nat/prime.lean
would have a bigger amount of imports.Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/nat.2Eprime
WIP because I might have to modify the imports of some files depending on
algebra.associated
.