Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: {Mv}Polynomial.algebraMap_apply simps #11193

Closed
wants to merge 26 commits into from
Closed

[Merged by Bors] - feat: {Mv}Polynomial.algebraMap_apply simps #11193

wants to merge 26 commits into from

Conversation

BoltonBailey
Copy link
Collaborator

@BoltonBailey BoltonBailey commented Mar 5, 2024 •
edited

  • Adds lemma Polynomial.algebraMap_eq analogous to MvPolynomial.algebraMap_eq
    • Adds some namespace disambiguations in various places to make this possible
  • Adds simp to these, and the related {Mv}Polynomial.algebraMap_apply lemmas.
    • Removes simp tag from later lemmas which linter says these additions now allow to be simp-proved

Open in Gitpod

@BoltonBailey BoltonBailey mentioned this pull request Mar 5, 2024
Open
1 task
@BoltonBailey BoltonBailey changed the title feat: Polynomial.algebraMap_eq_C feat: {Mv}Polynomial.algebraMap_apply simps Mar 6, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Mar 6, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. labels Mar 23, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@BoltonBailey BoltonBailey added awaiting-review The author would like community review of the PR awaiting-CI labels Mar 24, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Mar 24, 2024
@BoltonBailey BoltonBailey added the t-algebra Algebra (groups, rings, fields etc) label Mar 24, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 5, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 5, 2024
fpvandoorn
fpvandoorn approved these changes Apr 30, 2024
View reviewed changes
Copy link
Member

@fpvandoorn fpvandoorn left a comment •
edited

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This looks good to me, but it's outside the part of Mathlib I'm familiar with.

(note that the last commit is a clean merge into master)

maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by fpvandoorn.

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by fpvandoorn.

@riccardobrasca
Copy link
Member

Thanks!

bors merge

@riccardobrasca
Copy link
Member

bors r-

@mathlib-bors
Copy link

mathlib-bors bot commented Apr 30, 2024

Canceled.

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Apr 30, 2024
@riccardobrasca
Copy link
Member

Sorry, I didn't notice CI was still running.

bors d+

@mathlib-bors
Copy link

mathlib-bors bot commented Apr 30, 2024

✌️ BoltonBailey can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@fpvandoorn
Copy link
Member

The previous merge succeeded (it just shows an X because of the canceled bors run)

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Apr 30, 2024
@BoltonBailey @fpvandoorn
feat: {Mv}Polynomial.algebraMap_apply simps (#11193)
a0c4507 
* Adds lemma `Polynomial.algebraMap_eq` analogous to `MvPolynomial.algebraMap_eq`
  * Adds some namespace disambiguations in various places to make this possible 
* Adds `simp` to these, and the related `{Mv}Polynomial.algebraMap_apply` lemmas.
  * Removes simp tag from later lemmas which linter says these additions now allow to be simp-proved




Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@mathlib-bors
Copy link

mathlib-bors bot commented Apr 30, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: {Mv}Polynomial.algebraMap_apply simps [Merged by Bors] - feat: {Mv}Polynomial.algebraMap_apply simps Apr 30, 2024
@mathlib-bors mathlib-bors bot closed this Apr 30, 2024
@mathlib-bors mathlib-bors bot deleted the BoltonBailey/algebraMap_eq_C branch April 30, 2024 19:19
apnelson1 pushed a commit that referenced this pull request May 12, 2024
@BoltonBailey @fpvandoorn @apnelson1
feat: {Mv}Polynomial.algebraMap_apply simps (#11193)
b158e8c 
* Adds lemma `Polynomial.algebraMap_eq` analogous to `MvPolynomial.algebraMap_eq`
  * Adds some namespace disambiguations in various places to make this possible 
* Adds `simp` to these, and the related `{Mv}Polynomial.algebraMap_apply` lemmas.
  * Removes simp tag from later lemmas which linter says these additions now allow to be simp-proved




Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
callesonne pushed a commit that referenced this pull request May 16, 2024
@BoltonBailey @fpvandoorn @callesonne
feat: {Mv}Polynomial.algebraMap_apply simps (#11193)
11e6b3a 
* Adds lemma `Polynomial.algebraMap_eq` analogous to `MvPolynomial.algebraMap_eq`
  * Adds some namespace disambiguations in various places to make this possible 
* Adds `simp` to these, and the related `{Mv}Polynomial.algebraMap_apply` lemmas.
  * Removes simp tag from later lemmas which linter says these additions now allow to be simp-proved




Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@fpvandoorn fpvandoorn fpvandoorn approved these changes

Assignees
No one assigned
Labels
delegated maintainer-merge ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@BoltonBailey @leanprover-community-mathlib4-bot @riccardobrasca @fpvandoorn