Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
It’s not clear to me that its useful to have this as an entry separate from square root.
I think if you want the content of this entry to be find-able by readers, there should at least be more than a bare link from square root to it (at least a comment like: “For more discussion of … the reader may go to a dedicated entry real square root”).
It is not exactly clear that a principal square root function. defined on $[0, \infty)$ by the functional equation $\sqrt{x^2} = \vert x \vert$ as stated in the article, exists in a given set of real numbers in constructive mathematics.
As a result, I’ve asked for a proof of the existence of a principal square root function in a Cauchy complete Archimedean ordered field on this MathOverflow thread, and François G. Dorais provided a constructive real analytic proof of the existence of the principal square root function defined on $[0, \infty)$.
When I have the time, I’ll try to copy the proof over to the nlab, and credit Dorais appropriately, or if somebody else wants to do it before I do, they could go do it as well.
1 to 5 of 5