[Merged by Bors] - feat: simple lemmas about polynomials and their degrees #6220

adomani · 2023-07-28T16:36:03Z

This PR extracts some lemmas about polynomials that are helpful for the tactic compute_degree (#6221).

The signature of a theorem changed:

theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) :
    (p ^ m).coeff (n * m) = p.coeff n ^ m  -- <-- the order of the product was `n * m`
    (p ^ m).coeff (m * n) = p.coeff n ^ m  -- <-- and it became `m * n`

Modified files:

Data/Polynomial/Basic.lean
Data/Polynomial/Degree/Lemmas.lean
Data/Polynomial/Degree/Definitions.lean
Data/Polynomial/Coeff.lean  -- for a "`simp` can prove this" golf

depends on: [Merged by Bors] - chore(Algebra/{ Group/UniqueProds, Order/Monoid/Basic }): move eq_and_eq_of_le_of_le_of_mul_le earlier #6483, where eq_and_eq_of_le_of_le_of_mul_le moved earlier in the import hierarchy

Mathlib/Data/Polynomial/Basic.lean

ocfnash

Thanks, a few minor comments.

Mathlib/Data/Polynomial/Coeff.lean

Mathlib/Data/Polynomial/Degree/Lemmas.lean

Mathlib/Data/Polynomial/EraseLead.lean

…d_eq_of_le_of_le_of_mul_le` earlier (#6483) This move was suggested in #6220. In fact, the lemma is a general fact about an inequality involving multiplications and did not really belong in the file where it was. Affected files: ``` Algebra.Group.UniqueProds Algebra.Order.Monoid.Basic ```

Co-authored-by: Oliver Nash <github@olivernash.org>

leanprover-community-mathlib4-bot · 2023-08-10T10:21:08Z

This PR/issue depends on:

~~[Merged by Bors] - chore(Algebra/{ Group/UniqueProds, Order/Monoid/Basic }): move eq_and_eq_of_le_of_le_of_mul_le earlier #6483~~
By Dependent Issues (🤖). Happy coding!

ocfnash

Thanks!

Please apply the suggestions and then feel free to merge.

bors d+

Mathlib/Data/Polynomial/Degree/Definitions.lean

Mathlib/Data/Polynomial/Degree/Lemmas.lean

bors · 2023-08-10T10:42:04Z

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

Co-authored-by: Oliver Nash <github@olivernash.org>

adomani · 2023-08-10T11:59:12Z

bors r+

This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221). The signature of a theorem changed: ```lean theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) : (p ^ m).coeff (n * m) = p.coeff n ^ m -- <-- the order of the product was `n * m` (p ^ m).coeff (m * n) = p.coeff n ^ m -- <-- and it became `m * n` ``` Modified files: ``` Data/Polynomial/Basic.lean Data/Polynomial/Degree/Lemmas.lean Data/Polynomial/Degree/Definitions.lean Data/Polynomial/Coeff.lean -- for a "`simp` can prove this" golf ```

bors · 2023-08-10T13:44:19Z

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

…d_eq_of_le_of_le_of_mul_le` earlier (#6483) This move was suggested in #6220. In fact, the lemma is a general fact about an inequality involving multiplications and did not really belong in the file where it was. Affected files: ``` Algebra.Group.UniqueProds Algebra.Order.Monoid.Basic ```

This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221). The signature of a theorem changed: ```lean theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) : (p ^ m).coeff (n * m) = p.coeff n ^ m -- <-- the order of the product was `n * m` (p ^ m).coeff (m * n) = p.coeff n ^ m -- <-- and it became `m * n` ``` Modified files: ``` Data/Polynomial/Basic.lean Data/Polynomial/Degree/Lemmas.lean Data/Polynomial/Degree/Definitions.lean Data/Polynomial/Coeff.lean -- for a "`simp` can prove this" golf ```

…d_eq_of_le_of_le_of_mul_le` earlier (#6483) This move was suggested in #6220. In fact, the lemma is a general fact about an inequality involving multiplications and did not really belong in the file where it was. Affected files: ``` Algebra.Group.UniqueProds Algebra.Order.Monoid.Basic ```

This PR extracts some lemmas about polynomials that are helpful for the tactic `compute_degree` (#6221). The signature of a theorem changed: ```lean theorem coeff_pow_of_natDegree_le (pn : p.natDegree ≤ n) : (p ^ m).coeff (n * m) = p.coeff n ^ m -- <-- the order of the product was `n * m` (p ^ m).coeff (m * n) = p.coeff n ^ m -- <-- and it became `m * n` ``` Modified files: ``` Data/Polynomial/Basic.lean Data/Polynomial/Degree/Lemmas.lean Data/Polynomial/Degree/Definitions.lean Data/Polynomial/Coeff.lean -- for a "`simp` can prove this" golf ```

adomani mentioned this pull request Jul 28, 2023

[Merged by Bors] - feat: tactic compute_degree #6221

Closed

1 task

adomani added awaiting-review The author would like community review of the PR awaiting-CI t-algebra Algebra (groups, rings, fields etc) labels Jul 28, 2023

github-actions bot removed the awaiting-CI label Jul 28, 2023

j-loreaux reviewed Aug 1, 2023

View reviewed changes

Mathlib/Data/Polynomial/Basic.lean Show resolved Hide resolved

ocfnash reviewed Aug 9, 2023

View reviewed changes

ocfnash added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Aug 9, 2023

adomani added awaiting-review The author would like community review of the PR awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels Aug 9, 2023

github-actions bot removed the awaiting-CI label Aug 9, 2023

alreadydone reviewed Aug 9, 2023

View reviewed changes

Mathlib/Data/Polynomial/EraseLead.lean Outdated Show resolved Hide resolved

adomani mentioned this pull request Aug 10, 2023

[Merged by Bors] - chore(Algebra/{ Group/UniqueProds, Order/Monoid/Basic }): move eq_and_eq_of_le_of_le_of_mul_le earlier #6483

Closed

leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Aug 10, 2023

adomani and others added 8 commits August 10, 2023 12:14

Add lemmas of separate PR

5a405d4

Meld variables

a9e3110

Remove where

57751f3

Add simp attribute

1cb078d

Remove @[simp] on simpable lemma

118b8ed

Apply Oliver's suggestions

a8f2114

Apply suggestions from code review

16168ff

Co-authored-by: Oliver Nash <github@olivernash.org>

Relocate coeff_mul_add_of_le_natDegree_of_eq

6712a61

adomani force-pushed the adomani_compute_degree_lemmas branch from fb204dd to 6712a61 Compare August 10, 2023 10:16

leanprover-community-mathlib4-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. label Aug 10, 2023

ocfnash approved these changes Aug 10, 2023

View reviewed changes

Mathlib/Data/Polynomial/Degree/Definitions.lean Outdated Show resolved Hide resolved

Mathlib/Data/Polynomial/Degree/Lemmas.lean Outdated Show resolved Hide resolved

leanprover-community-mathlib4-bot added delegated and removed awaiting-review The author would like community review of the PR labels Aug 10, 2023

Apply suggestions from code review

69adb9f

Co-authored-by: Oliver Nash <github@olivernash.org>

bors bot changed the title ~~feat: simple lemmas about polynomials and their degrees~~ [Merged by Bors] - feat: simple lemmas about polynomials and their degrees Aug 10, 2023

bors bot closed this Aug 10, 2023

bors bot deleted the adomani_compute_degree_lemmas branch August 10, 2023 13:44

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat: simple lemmas about polynomials and their degrees #6220

[Merged by Bors] - feat: simple lemmas about polynomials and their degrees #6220

adomani commented Jul 28, 2023 •

edited

ocfnash left a comment

leanprover-community-mathlib4-bot commented Aug 10, 2023

ocfnash left a comment

bors bot commented Aug 10, 2023

adomani commented Aug 10, 2023

bors bot commented Aug 10, 2023

[Merged by Bors] - feat: simple lemmas about polynomials and their degrees #6220

[Merged by Bors] - feat: simple lemmas about polynomials and their degrees #6220

Conversation

adomani commented Jul 28, 2023 • edited

ocfnash left a comment

Choose a reason for hiding this comment

leanprover-community-mathlib4-bot commented Aug 10, 2023

ocfnash left a comment

Choose a reason for hiding this comment

bors bot commented Aug 10, 2023

adomani commented Aug 10, 2023

bors bot commented Aug 10, 2023

adomani commented Jul 28, 2023 •

edited