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(Data/Rat/NNRat): move module and algebra instances #9951
Conversation
We already have the instances for `ℕ`, `ℤ`, and `ℚ` in this file, so adding `NNRat` doesn't feel that out of place.
@@ -3,9 +3,10 @@ Copyright (c) 2022 Yaël Dillies, Bhavik Mehta. All rights reserved. | |||
Released under Apache 2.0 license as described in the file LICENSE. | |||
Authors: Yaël Dillies, Bhavik Mehta | |||
-/ | |||
import Mathlib.Algebra.Algebra.Basic | |||
import Mathlib.Algebra.Function.Indicator |
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.
Removing this would remove another 30 or so dependencies, but I'm declaring that a problem for a follow-up. I think further reduction probably entails splitting this file.
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.
Note that I already reduced the dependencies of Algebra.Function.Indicator
by quite a lot because of this.
I just noticed that maintainer merge |
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
Only before this PR though, 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.
Thanks 🎉
bors merge
Actually, this spurious dependency was introduced in #9950. |
As with #9950, this is motivated by: * Getting `NNRat` closed to `norm_num` * Being able to put an `nnrat_cast` field in `DivisionSemiring`s This brings down the number of dependencies of `NNRat` by around 600.
Build failed (retrying...): |
As with #9950, this is motivated by: * Getting `NNRat` closed to `norm_num` * Being able to put an `nnrat_cast` field in `DivisionSemiring`s This brings down the number of dependencies of `NNRat` by around 600.
Build failed (retrying...):
|
As with #9950, this is motivated by: * Getting `NNRat` closed to `norm_num` * Being able to put an `nnrat_cast` field in `DivisionSemiring`s This brings down the number of dependencies of `NNRat` by around 600.
Build failed: |
bors merge |
As with #9950, this is motivated by: * Getting `NNRat` closed to `norm_num` * Being able to put an `nnrat_cast` field in `DivisionSemiring`s This brings down the number of dependencies of `NNRat` by around 600.
Pull request successfully merged into master. Build succeeded: |
As with #9950, this is motivated by:
NNRat
closed tonorm_num
nnrat_cast
field inDivisionSemiring
sThis brings down the number of dependencies of
NNRat
by around 600.Archimedean
instances toOrder/Archimedean
#9950The graph is still a monster: