I am trying to find a good reference for a version of the implicit function theorem over $p$-adic manifolds. None of the texts I have consulted ( including "$p$-adic numbers, $p$-adic analysis, and Zeta functions" by Neal Koblitz and "$p$-adic analysis and Lie groups" by Peter Schneider) seem to discuss it. Of course, I can try to go through the argument in the real case and see if it works in the $p$-adic world, but it would be very desirable to have a reference. More precisely, I would like to know if a theorem of this type is true: Let $U$ and $V$ be open subsets of some $p$-adic manifolds and $f: U \to V$ a sufficiently smooth map defined on $U$ (From what I have seen, there seems to be a notion of strict differentiability in the $p$-adic setup. The function I will be interested are very nice, so most probably, I can live with a stronger assumption on $f$ too). If the rank of the derivative of $f$ at a point $x \in U$ is $r$, then after a smooth change of coordinates on possibly smaller open subsets of $U$ an $V$, $f$ can be expressed as $$f(x_1, \dots ,x_m)=(x_1, \dots , x_r, g_1(x), \dots , g_{n-r}(x)),$$ where $g_i$ are also smooth functions.
I would very much appreciate if someone can confirm that this is the case and point me to a reference.
