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

feat(data/mv_polynomial): add pderivative_eq_zero_of_not_mem_vars #2324

Merged

mergify merged 7 commits into master from pderivative-lemma

Apr 6, 2020

Collaborator

shingtaklam1324 commented Apr 4, 2020

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
reviewed and applied the documentation requirements
for tactics:
- added or adapted documentation in the tactic doc entries
- write an example of use of the new feature in test/tactics.lean or another test file
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

For reviewers: code review check list

Added the missing lemma from the previous PR:

lemma pderivative_eq_zero_of_not_mem_vars {v : S} {f : mv_polynomial S R} (h : v ∉ f.vars) :
  pderivative v f = 0 :=

shingtaklam1324 added 2 commits

April 4, 2020 21:26


          feat(data/mv_polynomial): add pderivative_eq_zero_of_not_mem_vars

c5a3ccf


          Added doc comment for pderivative.add_monoid_hom

be9ee1e

jcommelin reviewed

View reviewed changes

src/data/mv_polynomial.lean Outdated Show resolved Hide resolved


          Fix formatting

4798f7a

semorrison reviewed

View reviewed changes

src/data/mv_polynomial.lean Show resolved Hide resolved

semorrison reviewed

View reviewed changes

src/data/mv_polynomial.lean Outdated Show resolved Hide resolved

semorrison reviewed

View reviewed changes

src/data/mv_polynomial.lean Outdated Show resolved Hide resolved

semorrison reviewed

View reviewed changes

Collaborator

semorrison left a comment

Otherwise, looks great.

semorrison added the awaiting-author label


          fixed issues from review

581bb97

jcommelin reviewed

View reviewed changes

src/data/mv_polynomial.lean Outdated Show resolved Hide resolved


          change begin end to braces.

2d01bfd

jcommelin reviewed

View reviewed changes

src/data/mv_polynomial.lean Outdated Show resolved Hide resolved

jcommelin reviewed

View reviewed changes

src/data/mv_polynomial.lean Outdated Show resolved Hide resolved

jcommelin reviewed

View reviewed changes

src/data/mv_polynomial.lean Outdated Show resolved Hide resolved


          fix issues from review

4df9d43

jcommelin approved these changes

View reviewed changes

jcommelin added ready-to-merge and removed awaiting-author labels


          Merge branch 'master' into pderivative-lemma

1e6bb45

mergify bot merged commit 7b120a3 into master

mergify bot deleted the pderivative-lemma branch

April 6, 2020 18:21

anrddh pushed a commit to anrddh/mathlib that referenced this pull request


          feat(data/mv_polynomial): add pderivative_eq_zero_of_not_mem_vars (le…

d7780af

…anprover-community#2324)

* feat(data/mv_polynomial): add pderivative_eq_zero_of_not_mem_vars

* Added doc comment for `pderivative.add_monoid_hom`

* Fix formatting

* fixed issues from review

* change begin end to braces.

* fix issues from review

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

anrddh pushed a commit to anrddh/mathlib that referenced this pull request


          feat(data/mv_polynomial): add pderivative_eq_zero_of_not_mem_vars (le…

6bc6883

…anprover-community#2324)

* feat(data/mv_polynomial): add pderivative_eq_zero_of_not_mem_vars

* Added doc comment for `pderivative.add_monoid_hom`

* Fix formatting

* fixed issues from review

* change begin end to braces.

* fix issues from review

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request


          feat(data/mv_polynomial): add pderivative_eq_zero_of_not_mem_vars (le…

aaa2fba

…anprover-community#2324)

* feat(data/mv_polynomial): add pderivative_eq_zero_of_not_mem_vars

* Added doc comment for `pderivative.add_monoid_hom`

* Fix formatting

* fixed issues from review

* change begin end to braces.

* fix issues from review

Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment