Nat and left, right version of Int.sq_of_isCoprime

Stream: mathlib4

[Sabbir Rahman]

I was working on a olympiad problem that required proving a * b = c^2 with a, b coprime implies a, b are both squares. I found Int.sq_of_isCoprime, but no version of this for natural numbers. It's a bit of a nuissance to convert the natural number facts to integer apply Int.sq_of_isCoprime, then cancel out the negative square result etc. So any reason to not have the Nat version in mathlib? I'd be happy to add it if no issues

Also the Int.sq_of_isCoprime should have left and right version in my opinion, as that feels more like other theorems in mathlib.

[Ruben Van de Velde]

Yeah, that sounds welcome

[Sabbir Rahman]

Hmm, I was reading up on the sources related to this and it seems to me like documentation is not up to date. In particular these comments talk about results that are in a different file. I am kind of still new to contributing to mathlib, so not sure if I am correct. Am I correct?

[Kevin Buzzard]

Yes, PRs fixing docstrings are very much welcome! See e.g. #23245 for one of mine recently (also deleting a module docstring comment of the form "this definition is in this file" when it is no longer in the file)

[Kevin Buzzard]

Also, please feel to review docstring PRs if you feel confident about the material being discussed; everyone is welcome to review and approve PRs.

[Kim Morrison]

(Eventually we are going to switch over to Verso based doc-strings, and then these references in doc-strings to declarations and files will be checked in CI!)

[Sabbir Rahman]

Created #23369 to update the doc strings first :raised_hands:

[Sabbir Rahman]

a bit late, but I created 23677 for the original purpose of the thread.