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/mv_polynomial): cleanup equivs #6589
Conversation
src/data/mv_polynomial/equiv.lean
Outdated
-- TODO: move | ||
instance : is_scalar_tower R (mv_polynomial S₁ R) (polynomial (mv_polynomial S₁ R)) := | ||
finsupp.is_scalar_tower ℕ _ |
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.
Will remove these after #6592 is merged.
It looks very nice! Is it now possible to get rid of some |
Yes, I think after this PR every use of comap can be removed. |
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
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
This: * Replaces `alg_equiv_congr_left` with `rename_equiv` (to match `rename`) * Removes `ring_equiv_congr_left` (it's now `rename_equiv.to_ring_equiv`) * Renames `alg_equiv_congr_right` to `map_alg_equiv` (to match `map`) and removes the `comap` from the definition * Renames `ring_equiv_congr_right` to `map_equiv` (to match `map`) * Removes `alg_equiv_congr` (it's now `(map_alg_equiv R e).trans $ (rename_equiv e_var).restrict_scalars _`, which while longer is never used anyway) * Removes `ring_equiv_congr` (it's now `(map_equiv R e).trans $ (rename_equiv e_var).to_ring_equiv`, which while longer is never used anyway) * Replaces `punit_ring_equiv` with `punit_alg_equiv` * Removes `comap` from the definition of `sum_alg_equiv` * Promotes `option_equiv_left`, `option_equiv_right`, and `fin_succ_equiv` to `alg_equiv`s This is a follow-up to #6420
Build failed (retrying...): |
This: * Replaces `alg_equiv_congr_left` with `rename_equiv` (to match `rename`) * Removes `ring_equiv_congr_left` (it's now `rename_equiv.to_ring_equiv`) * Renames `alg_equiv_congr_right` to `map_alg_equiv` (to match `map`) and removes the `comap` from the definition * Renames `ring_equiv_congr_right` to `map_equiv` (to match `map`) * Removes `alg_equiv_congr` (it's now `(map_alg_equiv R e).trans $ (rename_equiv e_var).restrict_scalars _`, which while longer is never used anyway) * Removes `ring_equiv_congr` (it's now `(map_equiv R e).trans $ (rename_equiv e_var).to_ring_equiv`, which while longer is never used anyway) * Replaces `punit_ring_equiv` with `punit_alg_equiv` * Removes `comap` from the definition of `sum_alg_equiv` * Promotes `option_equiv_left`, `option_equiv_right`, and `fin_succ_equiv` to `alg_equiv`s This is a follow-up to #6420
Pull request successfully merged into master. Build succeeded: |
This: * Replaces `alg_equiv_congr_left` with `rename_equiv` (to match `rename`) * Removes `ring_equiv_congr_left` (it's now `rename_equiv.to_ring_equiv`) * Renames `alg_equiv_congr_right` to `map_alg_equiv` (to match `map`) and removes the `comap` from the definition * Renames `ring_equiv_congr_right` to `map_equiv` (to match `map`) * Removes `alg_equiv_congr` (it's now `(map_alg_equiv R e).trans $ (rename_equiv e_var).restrict_scalars _`, which while longer is never used anyway) * Removes `ring_equiv_congr` (it's now `(map_equiv R e).trans $ (rename_equiv e_var).to_ring_equiv`, which while longer is never used anyway) * Replaces `punit_ring_equiv` with `punit_alg_equiv` * Removes `comap` from the definition of `sum_alg_equiv` * Promotes `option_equiv_left`, `option_equiv_right`, and `fin_succ_equiv` to `alg_equiv`s This is a follow-up to #6420
This: * Replaces `alg_equiv_congr_left` with `rename_equiv` (to match `rename`) * Removes `ring_equiv_congr_left` (it's now `rename_equiv.to_ring_equiv`) * Renames `alg_equiv_congr_right` to `map_alg_equiv` (to match `map`) and removes the `comap` from the definition * Renames `ring_equiv_congr_right` to `map_equiv` (to match `map`) * Removes `alg_equiv_congr` (it's now `(map_alg_equiv R e).trans $ (rename_equiv e_var).restrict_scalars _`, which while longer is never used anyway) * Removes `ring_equiv_congr` (it's now `(map_equiv R e).trans $ (rename_equiv e_var).to_ring_equiv`, which while longer is never used anyway) * Replaces `punit_ring_equiv` with `punit_alg_equiv` * Removes `comap` from the definition of `sum_alg_equiv` * Promotes `option_equiv_left`, `option_equiv_right`, and `fin_succ_equiv` to `alg_equiv`s This is a follow-up to #6420
This:
alg_equiv_congr_left
withrename_equiv
(to matchrename
)ring_equiv_congr_left
(it's nowrename_equiv.to_ring_equiv
)alg_equiv_congr_right
tomap_alg_equiv
(to matchmap
) and removes thecomap
from the definitionring_equiv_congr_right
tomap_equiv
(to matchmap
)alg_equiv_congr
(it's now(map_alg_equiv R e).trans $ (rename_equiv e_var).restrict_scalars _
, which while longer is never used anyway)ring_equiv_congr
(it's now(map_equiv R e).trans $ (rename_equiv e_var).to_ring_equiv
, which while longer is never used anyway)punit_ring_equiv
withpunit_alg_equiv
comap
from the definition ofsum_alg_equiv
option_equiv_left
,option_equiv_right
, andfin_succ_equiv
toalg_equiv
sThis is a follow-up to #6420