Multivariate Hensel lemma for ultrametric fields (Q7027428)

This paper is part of a series of articles whose objective is to rewrite the theory of valued fields in constructive terms, without using non-constructive tools, commonly used in mathematics, such as Zorn's lemma or Law of excluded middle.\N\NIn this paper, the authors provide a direct constructive proof of the Multivariate Hensel Lemma for ultrametric discrete fields, without using the Zariski's Main Theorem.\N\NRecall that an ultrametric field \((K,|\cdot|)\) is an ultrametric discrete field if \(K\) is discret (there is a zero test) and if the disjunction \(|x| = 1\) or \(|x| < 1\) or \(|x| > 1\) is valid for all \(x \in K\). This amounts to saying that \(V\) is an integral residually discrete local ring.\N\NThus, given an ultrametric field \((K, |\cdot|)\) with a nontrivial absolute value, together with its separable closure \(\widetilde{K}\) in its completion \(\widehat{K}\), the authors prove first that given a Newton polynomial system \(F=(f_1, \ldots , f_n)\) at (\(\underline{0}\)) over \((V, m)\), it admits a unique zero with coordinates in \(\widetilde{m}\). Then, it's proved that \((K^H,V^H)\) is isomorphic to \((\widetilde{K},\widetilde{V} )\), where \((K^H,V^H)\) is the henselisation of \((K,V)\) constructed as in [\textit{F. V. Kuhlmann} and \textit{H. Lombardi}, J. Algebra 228, No. 2, 624--632 (2000; Zbl 0966.12004)].\N\NHence, from these two results, it's concluded that the system \(F\) also admits a unique zero with coordinates in \(mV^H\).