Take derivatives multiple times.

Stream: new members

[oishi]

image.png
Does anyone know how to translate the process in the image into Lean 4 code? Especially the part that involves taking derivatives multiple times.

[Ruben Van de Velde]

If you're formalizing these as polynomials, Polynomial.derivative^[k] p

[oishi]

Thanks a lot. And may I ask for another question? Do you know how to differentiate both sides of the equation in Lean4?Alternatively, is there a similar theorem existing in the field of polynomials?

[Ruben Van de Velde]

What kind of equation? A goal? A hypothesis?

[oishi]

image.png
As shown in this example, the given equation is

$$(1 - x)^n = \sum_{k=0}^n (-1)^k \binom{n}{k} x^k.$$

This is an already proven theorem. I would like to build upon this theorem to demonstrate that taking derivatives of both sides of the equation simultaneously will also yield equality.

[Ruben Van de Velde]

You can write something like

have h := existing_theorem n
apply_fun Polynomial.derivative^[k] at h

[oishi]

Thanks again. I will try.