Zulip Chat Archive
Stream: Is there code for X?
Topic: differentiation on `mv_polynomial`
Yury G. Kudryashov (Sep 10 2021 at 02:00):
Do we have a way to construct a differentiation on mv_polynomial by giving its values on the variables?
Yury G. Kudryashov (Sep 10 2021 at 02:02):
Sorry, I meant docs#derivation
Yury G. Kudryashov (Sep 10 2021 at 02:03):
It seems that we don't have much theory about derivations.
Yury G. Kudryashov (Sep 10 2021 at 02:04):
(outside of manifolds library)
Johan Commelin (Sep 10 2021 at 05:00):
@Shing Tak Lam is our derivation expert.
Johan Commelin (Sep 10 2021 at 05:01):
There is data/mv_polynomial/pderiv.lean, but it doesn't seem to use derivations.
Last updated: Dec 20 2023 at 11:08 UTC