-
Notifications
You must be signed in to change notification settings - Fork 298
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(ring_theory/polynomial/basic): remove a use of comap #6612
Conversation
This merges together `quotient_equiv_quotient_mv_polynomial` and `quotient_alg_equiv_quotient_mv_polynomial`, since the two now have the same domain and codomain.
I wanted to do it myself :D Otherwise it looks good to me. |
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.
For future reference, could you mention in the PR description why this works now? (Because there is some transitive algebra
instance that wasn't there before, right?)
bors d+
✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
This merges together `quotient_equiv_quotient_mv_polynomial` and `quotient_alg_equiv_quotient_mv_polynomial`, since the two now have the same domain and codomain. `comap` was previously needed here to provide a wrapper type with an R-algebra structure on `mv_polynomial σ (I.quotient)`. The updated `mv_polynomial.algebra` in #6533 transfers the `algebra R I.quotient` structure directly to `mv_polynomial σ I.quotient`, eliminating the need for this wrapper type.
Build failed (retrying...): |
This merges together `quotient_equiv_quotient_mv_polynomial` and `quotient_alg_equiv_quotient_mv_polynomial`, since the two now have the same domain and codomain. `comap` was previously needed here to provide a wrapper type with an R-algebra structure on `mv_polynomial σ (I.quotient)`. The updated `mv_polynomial.algebra` in #6533 transfers the `algebra R I.quotient` structure directly to `mv_polynomial σ I.quotient`, eliminating the need for this wrapper type.
Pull request successfully merged into master. Build succeeded: |
This merges together `quotient_equiv_quotient_mv_polynomial` and `quotient_alg_equiv_quotient_mv_polynomial`, since the two now have the same domain and codomain. `comap` was previously needed here to provide a wrapper type with an R-algebra structure on `mv_polynomial σ (I.quotient)`. The updated `mv_polynomial.algebra` in #6533 transfers the `algebra R I.quotient` structure directly to `mv_polynomial σ I.quotient`, eliminating the need for this wrapper type.
This merges together `quotient_equiv_quotient_mv_polynomial` and `quotient_alg_equiv_quotient_mv_polynomial`, since the two now have the same domain and codomain. `comap` was previously needed here to provide a wrapper type with an R-algebra structure on `mv_polynomial σ (I.quotient)`. The updated `mv_polynomial.algebra` in #6533 transfers the `algebra R I.quotient` structure directly to `mv_polynomial σ I.quotient`, eliminating the need for this wrapper type.
This merges together
quotient_equiv_quotient_mv_polynomial
andquotient_alg_equiv_quotient_mv_polynomial
, since the two now have the same domain and codomain.comap
was previously needed here to provide a wrapper type with an R-algebra structure onmv_polynomial σ (I.quotient)
.The updated
mv_polynomial.algebra
in #6533 transfers thealgebra R I.quotient
structure directly tomv_polynomial σ I.quotient
, eliminating the need for this wrapper type.