News for hackers. Stuff that matters.

A comment on Formalising a new proof that the square root of two is irrational. Parent comment

Re:Formalising a new proof that the square root of two is ir... by mannerheim on Thursday January 19, 2023 @11:10AM (#34441863)
The radical symbol always refers to a single-valued function by convention.

x^(1/n) is used for multi-valued functions in complex analysis, not the 'n-radical' symbol, which would usually refer to the principal root.

[ Parent | on HN ]
Re:Formalising a new proof that the square root of two is ir... by thehappypm on Thursday January 19, 2023 @01:32PM (#34443749)
Sure, but doesn’t that weaken the proof? It is an arbitrary restriction on the function that is required
[ Parent | on HN ]
Re:Formalising a new proof that the square root of two is ir... by mannerheim on Thursday January 19, 2023 @01:43PM (#34443885)
Barely? It proves it for the principal root, and you can trivially prove it for the negative root using the principal root's irrationality.
[ Parent | on HN ]