-
Notifications
You must be signed in to change notification settings - Fork 298
[Merged by Bors] - feat(ring_theory/ideal/operations): add an instance #6717
Conversation
@@ -1235,6 +1235,12 @@ by simp only [ring_hom.algebra_map_to_algebra, ring_hom.comp_id] | |||
instance {I : ideal A} : is_scalar_tower R A (ideal.quotient I) := | |||
is_scalar_tower.of_algebra_map_eq' (quotient.alg_map_eq R I) | |||
|
|||
instance quotient.is_scalar_tower' [algebra S A] [algebra S R] [is_scalar_tower S R A] |
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 think this one subsumes the instance above, so the one above can be removed. I doubt that will fix the timeout though.
Thanks for making the PR
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.
Indeed it doesn't...
If we want to keep this just for the record, should I close the PR?
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'll have a play with this tomorrow, now that you have a cache ready for me!
@eric-wieser should I close this or do you want to work on it? |
Well, I got CI passing on this (the failure was just a long line); I just haven't decided if it's actually a good idea. |
I can very well be wrong, but it seems to me a good instance to have. |
Oh nice, I hadn't realized that this enabled more golfing. |
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 think this is a useful instance, since the corresponding algebra S I.quotient
instance is already there. So I'll go ahead and merge this.
bors r+
This instance has been suggested by @eric-wieser in #6640. On my machine I get a deterministic timeout in `ring_theory/finiteness` at line 325, but in principle it seems a useful instance to have. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
This instance has been suggested by @eric-wieser in #6640. On my machine I get a deterministic timeout in `ring_theory/finiteness` at line 325, but in principle it seems a useful instance to have. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
This instance has been suggested by @eric-wieser in #6640.
On my machine I get a deterministic timeout in
ring_theory/finiteness
at line 325, but in principle it seems a useful instance to have.