Let $\mathcal{O}$ be the ring of valuation integers for a field complete with respect to a non-arch valuation | |. $f(X) \in \mathcal{O}[x]$. Let $f_j(X)$ be defined by the identity \begin{equation} f(X + Y) = f(X) + f_1(X)Y + f_2(X)Y^2 + ... \;\;\;\;\;\;\;\;\;\;\;\;\; (1) \end{equation}
Why does the above identity make sense? It seems to me non-obvious that the RHS converges.
Why is $f_1$ necessarily the formal derivative of $f$?
As the LHS of (1) is a polynomial therefore the RHS contains only finitely many terms so must converge. Expanding the LHS and equating coefficients of $y$ will give you $f_1 = f'$ as required.