[Merged by Bors] - feat:Polynomial.derivative_C_mul#19048
[Merged by Bors] - feat:Polynomial.derivative_C_mul#19048
Polynomial.derivative_C_mul#19048Conversation
PR summary 746c4e05b5Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as |
| derivative^[k] (C a * p) = C a * derivative^[k] p := by | ||
| simp_rw [← smul_eq_C_mul, iterate_derivative_smul] | ||
|
|
||
| theorem derivative_C_mul (a : R) (p : R[X]) : |
There was a problem hiding this comment.
| theorem derivative_C_mul (a : R) (p : R[X]) : | |
| @[simp] | |
| theorem derivative_C_mul (a : R) (p : R[X]) : |
There was a problem hiding this comment.
I found that this gives the following build(lint?) error link
/- The `simpNF` linter reports:
SOME SIMP LEMMAS ARE NOT IN SIMP-NORMAL FORM.
see note [simp-normal form] for tips how to debug this.
https://leanprover-community.github.io/mathlib_docs/notes.html#simp-normal%[20](https://github.com/leanprover-community/mathlib4/actions/runs/11844166189/job/33006753558?pr=19048#step:24:21)form -/
-- Mathlib.Algebra.Polynomial.Derivative
Error: ././././Mathlib/Algebra/Polynomial/Derivative.lean:149:1: error: @Polynomial.derivative_C_mul simp can prove this:
by simp only [@Polynomial.derivative_mul, @Polynomial.derivative_C, @zero_mul, @zero_add]
One of the lemmas above could be a duplicate.
If that's not the case try reordering lemmas or adding @[priority].
How can I fix this?
There was a problem hiding this comment.
Ah then ignore Johan's suggestion
There was a problem hiding this comment.
The error message is basically telling you that "this thing you're marking as @[simp] can itself be solved with simp (move it down to line 300 and see), so either don't mark this as simp or you're doing something wrong!"
|
✌️ seewoo5 can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
|
Pull request successfully merged into master. Build succeeded: |
Polynomial.derivative_C_mulPolynomial.derivative_C_mul
Add
Polynomial.derivative_C_mul. Note thatPolynomial.iterative_derivative_C_mulalready exists.Related: This exists as a lemma in #18882 now.