A multivariate Strassmann theorem

By a theorem of Strassmann, a non-zero convergent power series in one variable over a complete non-Archimedean field has finitely many zeros, with an explicit bound on their number. We generalize this result to convergent power series in several variables, characterizing finiteness of the zero set and bounding its cardinality in terms of the reduction of the saturated ideal defined by the power series. We discuss how to make our result effective, under suitable assumptions, when working with approximate power series.