PR summary 1c8be8adeb

Import changes for modified files

No significant changes to the import graph

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

Looking at this PR, it's descending a derivation on A to a derivation on M along a surjection, and the descent (possibly) depends on an auxiliary set-theoretic section. Is it true that the construction is independent of the choice of section?

Apologies, I don't know those terms. Are you asking if the defined derivation is independent of which inverse is taken? It is, because if f a = f b then f (a - b) = 0 so by hd f (d (a - b)) = 0, or f (d a) = f (d b)

I'm not quite sure on the theory behind this, this is my attempt to formalize (in more generality) "Now look at the natural surjective ring homomorphism F[X] -> F[x], which is the identity on F and sends X into x. Since F[x] = F(x) = K, the map D on F[X] will induce a derivation on K extending that on F if it so happens that D maps the kernel of our ring homomorphism into itself." from Maxwell Rosenlicht, Integration in Finite Terms, which I'm following for the proof of Liouville's theorem

Yeah, fair enough, it's a strange old result but the alternative is not to prove it at all and just prove it in the middle of your other argument when you need it, and this is not really the mathlib style. Maybe you could add a comment above the result just citing Rosenlicht to explain why it's needed? Then perhaps other people will be less confused when they see it. Finally, can you resolve the conversations which you've dealt with? That way it makes it much clearer that this PR is now pretty much ready.

bors d+

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

bors merge

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style