Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(data/mv_polynomial/funext): function extensionality for polynomials#4196

Closed
jcommelin wants to merge 15 commits intomasterfrom
poly-funext
Closed

[Merged by Bors] - feat(data/mv_polynomial/funext): function extensionality for polynomials#4196
jcommelin wants to merge 15 commits intomasterfrom
poly-funext

Conversation

@jcommelin
Copy link
Copy Markdown
Member

@jcommelin jcommelin commented Sep 21, 2020

over infinite integral domains

@jcommelin jcommelin added the awaiting-review The author would like community review of the PR label Sep 21, 2020
urkud
urkud reviewed Sep 21, 2020
View reviewed changes
urkud
urkud reviewed Sep 21, 2020
View reviewed changes
@urkud
Copy link
Copy Markdown
Member

urkud commented Sep 21, 2020

Otherwise LGTM.

jcommelin
jcommelin commented Sep 21, 2020
View reviewed changes
@urkud
Copy link
Copy Markdown
Member

urkud commented Sep 21, 2020

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Sep 21, 2020

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

@jcommelin
Copy link
Copy Markdown
Member Author

jcommelin commented Sep 22, 2020

@urkud I added function.injective.extend and golfed the proof of mv_polynomial.funext. Would you mind taking one more look?

bryangingechen
bryangingechen reviewed Sep 22, 2020
View reviewed changes
@jcommelin @bryangingechen
Update src/logic/function/basic.lean
53c0f4b 
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
urkud
urkud reviewed Sep 22, 2020
View reviewed changes
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 22, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 24, 2020
@jcommelin
Copy link
Copy Markdown
Member Author

jcommelin commented Sep 25, 2020

@urkud do you want to have another look? The bors d+ was from before the small refactor...

robertylewis
robertylewis reviewed Sep 25, 2020
View reviewed changes
@jcommelin @robertylewis
Update src/data/mv_polynomial/basic.lean
7a6bca5 
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
@urkud
Copy link
Copy Markdown
Member

urkud commented Sep 25, 2020

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Sep 25, 2020

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

jcommelin
jcommelin commented Sep 25, 2020
View reviewed changes
Copy link
Copy Markdown
Member Author

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Sep 25, 2020
bors bot pushed a commit that referenced this pull request Sep 25, 2020
@jcommelin
feat(data/mv_polynomial/funext): function extensionality for polynomi…
5deb96d 
…als (#4196)

over infinite integral domains
@bors
Copy link
Copy Markdown

bors bot commented Sep 25, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/mv_polynomial/funext): function extensionality for polynomials [Merged by Bors] - feat(data/mv_polynomial/funext): function extensionality for polynomials Sep 25, 2020
@bors bors bot closed this Sep 25, 2020
@bors bors bot deleted the poly-funext branch September 25, 2020 16:57
@kim-em kim-em mentioned this pull request Apr 3, 2023
Closed
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

3 more reviewers

@urkud urkud urkud left review comments

@robertylewis robertylewis robertylewis left review comments

@bryangingechen bryangingechen bryangingechen left review comments

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@jcommelin @urkud @robertylewis @bryangingechen