hasse derivative and homomorphism

Stream: maths

[Sham S]

lemma map_hasseDeriv_commutativity
    (P : K[X]) (i : ℕ): (P.map f).hasseDeriv i = (P.hasseDeriv i).map f := by
    ext n
    simp only [hasseDeriv_apply, coeff_map]

post this I'm unable to proceed, I'm new to lean and would like some help how to go from here, is this because apply sum results in different support, that is (P. map f) and the other is P.support

[Junyan Xu]

You code is missing imports and K, f are not defined. It doesn't work in the playground (online editor, see screenshot) so it's unlikely people can help you. Anyway, ext; simp [hasseDeriv_coeff] works, and this is now in google-deepmind/formal-conjectures#150.

image.png