[Merged by Bors] - feat(number_theory): pythagorean triples

[paulvanwamelen]

The classification of pythagorean triples (one of the "100 theorems")

---

[jcommelin]

Thanks for the PR! I left some comments.
I think that his PR should include some simp-lemmas about the circle parameterisation. If you apply the equiv to a term of k, what does the result look like? (I know the answer, but simp doesn't.) Similarly, if you have a point on the circle, and you apply the equiv.symm, which element of k do you get?

[paulvanwamelen]

Are these the simp lemmas you had in mind:

lemma circle_equiv_inv (hk : ∀ x : K, 1 + x^2 ≠ 0) (v : K) (w : K) (hp : v^2 + w^2 = 1 ∧ w ≠ -1) :
  (circle_equiv_gen hk).inv_fun ⟨⟨v, w⟩, hp⟩ = v / (w + 1) := by refl

lemma circle_equiv_fun (hk : ∀ x : K, 1 + x^2 ≠ 0) (x : K) :
  ((circle_equiv_gen hk).to_fun x).val = ⟨2 * x / (1 + x^2), (1 - x^2) / (1 + x^2)⟩ := by refl

?

[jcommelin]

Are these the simp lemmas you had in mind:

lemma circle_equiv_inv (hk : ∀ x : K, 1 + x^2 ≠ 0) (v : K) (w : K) (hp : v^2 + w^2 = 1 ∧ w ≠ -1) :
  (circle_equiv_gen hk).inv_fun ⟨⟨v, w⟩, hp⟩ = v / (w + 1) := by refl

lemma circle_equiv_fun (hk : ∀ x : K, 1 + x^2 ≠ 0) (x : K) :
  ((circle_equiv_gen hk).to_fun x).val = ⟨2 * x / (1 + x^2), (1 - x^2) / (1 + x^2)⟩ := by refl

?

Almost, yes. But replace inv_fun with symm, and let ((v,w), hp) be an arbitrary term of the subtype: (x : { p : K × K // ... }).
Remove .to_fun, and replace .val by a coercion.

[jcommelin]

I suggest adding a bit more material to the pythagorean triples file. How much extra work (lines of code) do you think the classification is?

[paulvanwamelen]

The whole file is currently 500 lines. I can add about 200 more lines of silly lemmas that are needed. Or should I just add the whole thing?

[jcommelin]

Maybe just add the whole thing, if you don't need any changes to other files. Otherwise, I suggest a "preparations for" PR, that does all the changes you need to existing files, and then a "new file" PR.

[paulvanwamelen]

OK, I'll add the rest now. I don't need more changes to other files.

[semorrison]

@paulvanwamelen, I can see you've marked this as request-review again, but there are many unresolved conversations above, so it's hard for me to review this without having to re-read everything. Could you please mark all resolved conversations as resolved, and if there are any outstanding ones (or ones where'd you like someone else to confirm they've successfully been resolved), comment on them?

[semorrison]

There are also some linting errors that need to be fixed.

[paulvanwamelen]

I haven't had time to properly look at this, but the linter complains that the definition of is_classified and is_primitive_classified doesn't depend on the fact that x y and z form a pythagorean triple. And, of course, the linter is correct: is_classified is just a property of x and y. On the other hand it is nice to be able to say h.is_classified. So what should be done? Include something like x * x + y * y = z * z in the condition for is_classified? Or just tell the linter to ignore the problem?

[paulvanwamelen]

I closed most comments. There are one or 2 still open above, some for me and one for Scott.

[jcommelin]

@paulvanwamelen Just add @[nolint unused_arguments] before those definitions.

[paulvanwamelen]

I believe everything has been addressed now. Ready for another review.

[jcommelin]

This is looking good now! Almost ready for merging.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Lint mathlib
• Run tests and docs
• Build mathlib