[Merged by Bors] - feat(Data/Polynomial/Derivation): add version of chain rule by rmhi · Pull Request #7419 · leanprover-community/mathlib4

rmhi · 2023-09-28T12:25:39Z

If A is an R-algebra and d : A → M is a derivation, then for any polynomial f : R[X] and any a : A,
d(f(a)) = f'(a) d a.

There are shorter proofs of this result, but in my view the most sensible proof is to interpret both sides of
the equation as derivations R[X] \to M, and then to check that they agree in the case f = X.

riccardobrasca · 2023-10-16T08:57:27Z

Can you split the PR in two, opening another one with only the R[X]-module structure? It is an important construction (thanks for adding it!) and it deserves its own discussion. Feel free to ask my review.

…map. (#7728) Given an element `a` in an `R`-algebra `A` and an `A`-module `M`, define an `R[X]`-module `Module.AEval R M a`, whose elements correspond to elements of `M`, and where the action of `f : R[X]` is `f • m = aeval a f • m`. Equivalently, `X • m = a • m`. This module is abbreviated to `Module.AEval' φ` in the special case that `A` is the algebra of `R`-linear maps and `φ : M → M` is an `R`-linear map. This is needed in #7419. Co-authored-by: Richard M. Hill <86743862+rmhi@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Co-authored-by: Johan Commelin <johan@commelin.net>

jcommelin · 2023-11-03T14:44:55Z

bors d+

bors · 2023-11-03T14:44:57Z

✌️ rmhi 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 · 2023-11-03T15:00:18Z

In fact, this seems completely ready for merging, so:

Thanks 🎉

bors merge

eric-wieser · 2023-11-03T15:06:01Z

This will have conflicts with #8151, as the name of the simps lemma changes.

If `A` is an `R`-algebra and `d : A → M` is a derivation, then for any polynomial `f : R[X]` and any `a : A`, `d(f(a)) = f'(a) d a`. Co-authored-by: Richard M. Hill <86743862+rmhi@users.noreply.github.com>

eric-wieser · 2023-11-03T15:59:08Z

bors r-

bors · 2023-11-03T15:59:10Z

Canceled.

rmhi · 2023-11-03T16:26:34Z

This will have conflicts with #8151, as the name of the simps lemma changes.

If I change the name from toFun to apply on line 150, then I assume this will be ok, except that the code will not work until #8151 is merged. How should I proceed?

eric-wieser · 2023-11-03T16:46:21Z

Yes, if you make that change I'm happy for you to put this on the queue even though CI will fail; as you say, it will succeed when it lands.

eric-wieser · 2023-11-03T16:47:44Z

Alternatively, if you wait 5 minutes you can just merge master :)

eric-wieser · 2023-11-03T17:06:08Z

bors merge

If `A` is an `R`-algebra and `d : A → M` is a derivation, then for any polynomial `f : R[X]` and any `a : A`, `d(f(a)) = f'(a) d a`. Co-authored-by: Richard M. Hill <86743862+rmhi@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

ocfnash · 2023-11-03T19:30:06Z

GitHub was flaking and bors crashed so we need to try this again

bors merge

If `A` is an `R`-algebra and `d : A → M` is a derivation, then for any polynomial `f : R[X]` and any `a : A`, `d(f(a)) = f'(a) d a`. Co-authored-by: Richard M. Hill <86743862+rmhi@users.noreply.github.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

bors · 2023-11-03T21:31:35Z

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.

rmhi added 6 commits September 27, 2023 13:47

initial commit

47ddf0e

added unused instances

5a6f3ee

try one fewer

f3a47f9

try one fewer again

14cf29c

switched to aeval

1916403

tidying up

a579d6e

rmhi added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Sep 28, 2023

github-actions Bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Sep 28, 2023

rmhi added the awaiting-review label Sep 28, 2023

eric-wieser reviewed Sep 28, 2023

View reviewed changes

Comment thread Mathlib/Data/Polynomial/Derivation.lean Outdated

eric-wieser reviewed Sep 28, 2023

View reviewed changes

Comment thread Mathlib/Data/Polynomial/Derivation.lean Outdated

eric-wieser reviewed Sep 28, 2023

View reviewed changes

Comment thread Mathlib/Data/Polynomial/Derivation.lean Outdated

rmhi added 3 commits September 28, 2023 20:14

changes suggested by review

fa647b3

tidying up

7812757

added docstrings

a87e7dc

riccardobrasca reviewed Oct 4, 2023

View reviewed changes

Comment thread Mathlib/Data/Polynomial/Derivation.lean Outdated

jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Oct 12, 2023

changes following review

4f9d565

rmhi added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Oct 14, 2023

rmhi requested a review from riccardobrasca October 15, 2023 19:41

rmhi added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed awaiting-review labels Oct 17, 2023

ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Oct 17, 2023

erdOne mentioned this pull request Oct 17, 2023

[Merged by Bors] - feat(Data/Polynomial/Module) : define an R[X] module, given a linear map. #7728

Closed

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 1, 2023

rmhi added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 2, 2023

jcommelin added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 3, 2023

rmhi and others added 2 commits November 3, 2023 10:25

Update Mathlib/Data/Polynomial/Derivation.lean

d37220f

Co-authored-by: Johan Commelin <johan@commelin.net>

corrections following review

1cfa5ae

eric-wieser reviewed Nov 3, 2023

View reviewed changes

Comment thread Mathlib/Data/Polynomial/Derivation.lean Outdated

correction to comment

05788bd

rmhi added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Nov 3, 2023

github-actions Bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Nov 3, 2023

github-actions Bot added the ready-to-merge This PR has been sent to bors. label Nov 3, 2023

rmhi and others added 2 commits November 3, 2023 16:51

change toFun to apply

cab2f3c

Merge remote-tracking branch 'origin/master' into eval2-chain-rule

6438ff5

bors Bot changed the title ~~feat(Data/Polynomial/Derivation): add version of chain rule~~ [Merged by Bors] - feat(Data/Polynomial/Derivation): add version of chain rule Nov 3, 2023

bors Bot closed this Nov 3, 2023

bors Bot deleted the eval2-chain-rule branch November 3, 2023 21:31

Uh oh!

Conversation

rmhi commented Sep 28, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

riccardobrasca commented Oct 16, 2023

Uh oh!

Uh oh!

jcommelin commented Nov 3, 2023

Uh oh!

bors Bot commented Nov 3, 2023

Uh oh!

jcommelin commented Nov 3, 2023

Uh oh!

eric-wieser commented Nov 3, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

eric-wieser commented Nov 3, 2023

Uh oh!

bors Bot commented Nov 3, 2023

Uh oh!

rmhi commented Nov 3, 2023

Uh oh!

eric-wieser commented Nov 3, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

eric-wieser commented Nov 3, 2023

Uh oh!

eric-wieser commented Nov 3, 2023

Uh oh!

ocfnash commented Nov 3, 2023

Uh oh!

bors Bot commented Nov 3, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

5 participants

rmhi commented Sep 28, 2023 •

edited

Loading

eric-wieser commented Nov 3, 2023 •

edited

Loading

eric-wieser commented Nov 3, 2023 •

edited

Loading