Local Bézout Theorem

We give an elementary proof of what we call the Local Bézout Theorem. Given a system of n polynomials in n indeterminates with coefficients in a Henselian local domain, , which residually defines an isolated point in of multiplicity r, we prove (under some additional hypothesis on ) that there are finitely many zeroes of the system above the residual zero (i.e., with coordinates in m), and the sum of their multiplicities is r. Our proof is based on techniques of computational algebra.