Zulip Chat Archive

Stream: Is there code for X?

Topic: General leibniz

Calle Sönne (Sep 03 2024 at 10:25):

Do we have the general Leibniz rule in mathlib in some form?

Yaël Dillies (Sep 03 2024 at 10:52):

In terms of docs#Derivation ?

Calle Sönne (Sep 03 2024 at 10:53):

Whichever, I am mainly interested in the proof (I am currently proving the corresponding statement for LieDerivations).

Sébastien Gouëzel (Sep 03 2024 at 11:05):

We have the inequality, for the Fréchet derivative, in docs#norm_iteratedFDerivWithin_mul_le

Last updated: May 02 2025 at 03:31 UTC