Squarefree numbers and irrational square roots

Stream: Is there code for X?

[Richard Zandi]

Hi! I've been working on connecting squarefree numbers to irrationality and have these theorems:

lemma squarefree_not_isSquare {m : ℕ} (hsq : Squarefree m) (h1 : 1 < m) : ¬ IsSquare m

lemma irrational_sqrt_of_squarefree (m : ℕ) (hsq : Squarefree m) (h1 : 1 < m) :
    Irrational (Real.sqrt m)

lemma squarefree_ten : Squarefree 10

lemma irrational_sqrt_ten : Irrational (Real.sqrt 10)

Is there already something like this in Mathlib4? The general theorem irrational_sqrt_of_squarefree seems like it could be useful - it gives a clean way to prove irrationality of √n for any squarefree n > 1.

If this would be a welcome addition, I'd like to submit a PR!

[Matt Diamond]

docs#irrational_sqrt_natCast_iff might cover this already (or at least it covers the 2nd step once you've proved the first)

[Matt Diamond]

not sure if you're aware, but Irrational (Real.sqrt m) for some (m : ℕ) is actually decidable in Lean, so the following works:

import Mathlib

example : Irrational (Real.sqrt 10) := by decide

[Richard Zandi]

Thanks Matt!

Right on both points. I tested by decide and it works perfectly for Irrational (Real.sqrt 10) - much cleaner than my manual proof.

And irrational_sqrt_natCast_iff provides the ¬IsSquare n → Irrational √n direction I was using.

The novel part is really squarefree_not_isSquare : Squarefree m → ¬IsSquare m, which provides the missing link. Combined with the existing irrational_sqrt_natCast_iff, this gives a systematic way to prove irrationality via the squarefree property.

Would squarefree_not_isSquare still be worth contributing as the key bridging theorem?

[Kevin Buzzard]

"the square root of a squarefree natural bigger than 1 is irrational" is a strictly weaker statement than "the square root of a nonsquare natural is irrational" and we have the latter already.

[Kevin Buzzard]

squarefree_not_isSquare is a relatively straightforward consequence of the stronger Nat.squarefree_pow_iff but you might be able to get the statement into Data.Nat.Squarefree I guess?

[Richard Zandi]

Thanks

I see that squarefree_not_isSquare would be a convenience lemma rather than filling a gap. Would it be worth adding to Data.Nat.Squarefree as a straightforward application of Nat.squarefree_pow_iff?

[Kevin Buzzard]

You can try it, it might just get shooed through or people might ask why you need it, it's difficult for me to guess what will happen. I usually only PR stuff which I need in big projects but other people do things differently.