Explicit computation of a Fréchet derivative

Stream: mathlib4

[Xavier Roblot]

I need to compute the Fréchet derivative of a function of several variables, say $f : ℝ^{n+1} → ℝ$
defined by $f(x) = x_0 ∏ n_i^{x_i}$ where the $n_i$'s are some fixed
positive reals. I am correct to assume that the best way to proceed is to use
docs#hasFDerivAt_iff_isLittleO_nhds_zero and then do some little o computations or is there a better way to proceed?

[Xavier Roblot]

Hum, actually I found docs#HasFDerivAt.finset_prod which might be more adapted