News for hackers. Stuff that matters.
Re:Formalising a new proof that the square root of two is ir... by DNied on Thursday January 19, 2023 @09:48AM (#34440844)
You forget that √x always has 2 solutions: 1 positive and 1 negative.
Re:Formalising a new proof that the square root of two is ir... by johnnny on Thursday January 19, 2023 @10:18AM (#34441195)
It's very obvious in context that they meant the positive solution of xˆ2 = 2.

My definition of the square root is as follows: the square root of a positive real number x is the positive number, noted √x, such that (√x) ^ 2 = x. To make this a useable definition, we need to prove that equation has a solution (using the fact the function t -> t^2 is zero for t=0, diverges to +inf when t -> +inf, and is continuous between the two) and that solution is unique (using the fact the same function is strictly increasing).

Do you have any other definition of √x?

Re:Formalising a new proof that the square root of two is ir... by zeroonetwothree on Thursday January 19, 2023 @10:47AM (#34441553)
The sqrt symbol is defined as the positive root
Re:Formalising a new proof that the square root of two is ir... by syzarian on Thursday January 19, 2023 @12:43PM (#34443160)
The equation :

x^2 = a

where a is a positive real number has two solutions. An equation can have multiple solutions (even infinitely many solutions). Sqrt(x) is a function and as such it can have only one output for a given input. Functions don’t have solutions. By definition, sqrt(a) is the nonnegative solution of the equation x^2=a. Here, a can be zero.