Zulip Chat Archive

With the search methods I know I did not find any definition of derivation in Mathlib. There is not any right? In case not should I start from scratch or is there some more general structure that I can get derivations as a particular case or some non obvious structure I can extend (with obvious I mean the ones one would clearly think about by looking at Wikipedia's definition)? I did not really work with anything in the algebra section so it'd be cool to listen to some tips before beginning

Patrick Massot (Jul 10 2020 at 11:15):

I think @Shing Tak Lam did something in this direction.

Kevin Buzzard (Jul 10 2020 at 11:15):

@Kenny Lau wrote some code on Zulip about a year ago but never made a PR

Kevin Buzzard (Jul 10 2020 at 11:16):

Shing did partial derivatives of multivariate polynomials and I'm pretty sure this got PRed

Kevin Buzzard (Jul 10 2020 at 11:17):

But this is definitely something which could be in mathlib. Module of Kaehler differentials and its universal property would be really nice to do

Shing Tak Lam (Jul 10 2020 at 11:26):

Patrick Massot said:

I think Shing Tak Lam did something in this direction.

I guess there's this?

Patrick Massot (Jul 10 2020 at 11:26):

Oh this is already specialized to polynomials :sad:

Kevin Buzzard (Jul 10 2020 at 11:27):

That's because Shing is a schoolkid so I thought that leaping into the general theory of modules and derivations might not have been appropriate :rolling_on_the_floor_laughing: