News for hackers. Stuff that matters.
Re:Formalising a new proof that the square root of two is ir... by perihelions on Thursday January 19, 2023 @11:05AM (#34441783)
Right. It can also generalize for any non-integral square root of an integer √n. Let a be the integer ⌊√n⌋, such that a < √n < a+1 -- strict inequalities, because √n is non-integral. So 0 < √n - a < 1 and the same proof works with

    k' = √n k - a k         (instead of √2 k - 1 k)
       = k(√n - a)          (so 0 < k' < k)

    √n k' = n k - a k √n    (is integral; k' ∈ K)

There are no comments on this comment yet.