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: MvPolynomial.X_ne_zero #11071

Closed

BoltonBailey wants to merge 1 commit into master from BoltonBailey/x-ne-zero

Collaborator

BoltonBailey commented Feb 29, 2024

Proves that a variable is not the zero polynomial, analogous to Polynomial.X_ne_zero.


          prove theorem

d2b7001

BoltonBailey added awaiting-CI easy and removed easy labels

github-actions bot removed the awaiting-CI label

BoltonBailey added the awaiting-review label

Collaborator Author

BoltonBailey commented Feb 29, 2024

Is there any reason this shouldn't be simp? The single-variable version is not, but it seems useful if it's allowed.

Member

riccardobrasca commented Mar 1, 2024

Is there any reason this shouldn't be simp? The single-variable version is not, but it seems useful if it's allowed.

How can simp use a ≠ lemma?

Member

riccardobrasca commented Mar 1, 2024

Is there any reason this shouldn't be simp? The single-variable version is not, but it seems useful if it's allowed.

How can simp use a ≠ lemma?

Well, it can of course close the goal X ≠ 0...

Collaborator

Ruben-VandeVelde commented Mar 1, 2024

maintainer merge

github-actions bot commented Mar 1, 2024

🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde.

github-actions bot added the maintainer-merge label

jcommelin approved these changes

View reviewed changes

Member

jcommelin left a comment

Thanks 🎉

bors merge

leanprover-community-mathlib4-bot added ready-to-merge and removed awaiting-review labels

Member

riccardobrasca commented Mar 1, 2024

Can you add the simp attribute also to one variable case? In another PR it's fine.

mathlib-bors bot pushed a commit that referenced this pull request


          feat: MvPolynomial.X_ne_zero (#11071)

37684c2

Proves that a variable is not the zero polynomial, analogous to `Polynomial.X_ne_zero`.

mathlib-bors bot commented Mar 1, 2024

Build failed (retrying...):

Build

mathlib-bors bot pushed a commit that referenced this pull request


          feat: MvPolynomial.X_ne_zero (#11071)

25d9b37

Proves that a variable is not the zero polynomial, analogous to `Polynomial.X_ne_zero`.

mathlib-bors bot commented Mar 1, 2024

Pull request successfully merged into master.

Build succeeded:

mathlib-bors bot changed the title ~~feat: MvPolynomial.X_ne_zero~~ [Merged by Bors] - feat: MvPolynomial.X_ne_zero

mathlib-bors bot closed this

mathlib-bors bot deleted the BoltonBailey/x-ne-zero branch

March 1, 2024 17:22

BoltonBailey mentioned this pull request

[Merged by Bors] - chore: add simp to Polynomial.X_ne_zero #11101

Closed

mathlib-bors bot pushed a commit that referenced this pull request


          chore: add simp to Polynomial.X_ne_zero (#11101)

0eb97a5

As requested [here](#11071 (comment)) by @riccardobrasca

kbuzzard pushed a commit that referenced this pull request


          feat: MvPolynomial.X_ne_zero (#11071)

40135bb

Proves that a variable is not the zero polynomial, analogous to `Polynomial.X_ne_zero`.

kbuzzard pushed a commit that referenced this pull request


          chore: add simp to Polynomial.X_ne_zero (#11101)

6ba9826

As requested [here](#11071 (comment)) by @riccardobrasca

dagurtomas pushed a commit that referenced this pull request


          feat: MvPolynomial.X_ne_zero (#11071)

23dd5de

Proves that a variable is not the zero polynomial, analogous to `Polynomial.X_ne_zero`.

dagurtomas pushed a commit that referenced this pull request


          chore: add simp to Polynomial.X_ne_zero (#11101)

c62b5ed

As requested [here](#11071 (comment)) by @riccardobrasca

utensil pushed a commit that referenced this pull request


          feat: MvPolynomial.X_ne_zero (#11071)

4f2378a

Proves that a variable is not the zero polynomial, analogous to `Polynomial.X_ne_zero`.

utensil pushed a commit that referenced this pull request


          chore: add simp to Polynomial.X_ne_zero (#11101)

e40e4f8

As requested [here](#11071 (comment)) by @riccardobrasca

Louddy pushed a commit that referenced this pull request


          feat: MvPolynomial.X_ne_zero (#11071)

ea91810

Proves that a variable is not the zero polynomial, analogous to `Polynomial.X_ne_zero`.

Louddy pushed a commit that referenced this pull request


          chore: add simp to Polynomial.X_ne_zero (#11101)

1c6f3f9

As requested [here](#11071 (comment)) by @riccardobrasca

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