## Stream: new members

### Topic: Pythagorean triples

#### Paul van Wamelen (May 24 2020 at 20:51):

I have a proof of the formula for Pythagorean triples (Number 23 on the 100 Theorems list). I would like to PR this to mathlib. Where should it go though? In src\number_theory or archive\100-theorems-list?
I've made a PR for the first lemma needed in multiset. Hope I did it right! Feedback would be appreciated. I probably still have a lot of cleanup to do...

#### Alex J. Best (May 24 2020 at 21:15):

I would say in number theory rather than archive, this formula could be useful in other developments.

#### Yury G. Kudryashov (May 24 2020 at 23:39):

Do you prove rational parametrization of the circle?

#### Jalex Stark (May 25 2020 at 00:48):

Yury G. Kudryashov said:

Do you prove rational parametrization of the circle?

Is that the same as characterizing all pythagorean triples and then dividing so one side of the equation is 1?

#### Kevin Buzzard (May 25 2020 at 00:51):

Parametrising the circle is easier, it's less fiddly. You want to find all solutions to $x^2+y^2=1$ in rationals, and you use the fact that each solution $(a,b)$ lies on a unique line which also goes through $(1,0)$, so you just consider lines of the form $y=m(x-1)$ for a fixed $m$; this is two equations in the two unknowns $x$ and $y$ which simplify to one quadratic equation in $x$ and you know $x=1$ is a root, and you can read off the sum of the roots, so you get $a$ from this, and then $b$ by the linear equation. Now clear denominators to get the "classical" result.

#### Paul van Wamelen (May 25 2020 at 01:55):

This seems much simpler than going through the gaussian integers (which is what I did)...

#### Yury G. Kudryashov (May 25 2020 at 03:10):

As a free bonus you get the equivalence for any field with ∀ x, x^2+1 ≠ 0 (in particular, any linear ordered field).

#### Yury G. Kudryashov (May 25 2020 at 03:20):

Something like (with sorrys and a suboptimal proof):

variables {k : Type*} [field k]

def circle_equiv_gen (hk : ∀ x : k, 1 + x^2 ≠ 0) :
k ≃ {p : k × k | p.1^2 + p.2^2 = 1 ∧ p.2 ≠ -1} :=
{ to_fun := λ x, ⟨⟨2 * x / (1 + x^2), (1 - x^2) / (1 + x^2)⟩,
by { field_simp [hk x, div_pow], ring },
by { simp only [ne.def, div_eq_iff (hk x), ← neg_mul_eq_neg_mul, one_mul, neg_add,
convert hk 1,
simp }⟩,
inv_fun := λ p, p.1.1 / (p.1.2 + 1),
left_inv := λ x, by { field_simp [hk x], sorry },
right_inv := λ ⟨⟨x, y⟩, hxy, hy⟩, sorry
}


#### Kevin Buzzard (May 25 2020 at 09:13):

The parametrisation trick works for any smooth plane conic over any field, showing they're birational and hence isomorphic to $\mathbb{P}^1$.

#### Paul van Wamelen (Jun 21 2020 at 19:14):

I've now followed the suggestion to use the rational parametrization of the the circle to do pythagorean triples. It actually turns out to be VERY fiddly. There is a problem with divisibility by 2 when you want to go from x/z = (m^2-n^2)/(m^2+y^2) to x = m^2 - n^2. Anyway, that isn't my question. Should something like this:

lemma rat_id {a b c d : ℤ} (hb0 : 0 < b) (hd0 : 0 < d) (h1 : nat.coprime a.nat_abs b.nat_abs)
(h2 : nat.coprime c.nat_abs d.nat_abs) (h : (a : ℚ) / b = (c : ℚ) / d) :
a = c ∧ b = d


go in data\rat\basic.lean? What should this be named, rat_id is probably not right.

#### Paul van Wamelen (Jun 21 2020 at 19:19):

I prove that by first proving (the even more poorly named):

import data.rat.basic
import data.int.gcd
import tactic

lemma rat_id0 {a b : ℤ} (hb0 : 0 < b) (h : nat.coprime a.nat_abs b.nat_abs) :
a = ((a : ℚ) / b).num ∧ b = ((a : ℚ) / b).denom :=
begin
have h2 : (a : ℚ) / b = rat.mk ((a : ℚ) / b).num ((a : ℚ) / b).denom, { rw rat.num_denom },
rw ←rat.mk_eq_div at h2,
have h3 : a * ((a : ℚ) / b).denom = ((a : ℚ) / b).num * b,
{ apply (rat.mk_eq _ _).1, rw h2,
rw ←rat.mk_eq_div, exact (ne_of_lt hb0).symm,
simp only [rat.denom_ne_zero, int.coe_nat_eq_zero, ne.def, not_false_iff] },
have h4 : int.nat_abs b ∣ int.nat_abs (a * ((a : ℚ) / b).denom),
{ exact int.nat_abs_dvd_abs_iff.2 (dvd_of_mul_left_eq _ h3.symm) },
have h5 : int.nat_abs b ∣ int.nat_abs a * ((a : ℚ) / b).denom, { rw int.nat_abs_mul at h4, exact h4 },
have h6 : int.nat_abs b ∣ ((a : ℚ) / b).denom,
{ apply nat.coprime.dvd_of_dvd_mul_left (nat.coprime.symm h) h5 },
have h7 : ((a : ℚ) / b).denom ∣ int.nat_abs ((a : ℚ) / b).num * int.nat_abs b,
{ rw ←int.nat_abs_mul,
change int.nat_abs ((a : ℚ) / b).denom ∣ int.nat_abs (((a : ℚ) / b).num * b),
apply int.nat_abs_dvd_abs_iff.2,
apply dvd_of_mul_left_eq _ h3
},
have h8 : ((a : ℚ) / b).denom ∣ int.nat_abs b,
{ exact nat.coprime.dvd_of_dvd_mul_left (nat.coprime.symm ((a : ℚ) / b).cop) h7 },
have h9 : ((a : ℚ) / b).denom = int.nat_abs b, { exact nat.dvd_antisymm h8 h6 },
have h10 : (((a : ℚ) / b).denom : ℤ) = b,
{ rw [int.eq_nat_abs_of_zero_le (le_of_lt hb0)] {occs := occurrences.pos }, rw h9 },
apply and.intro _ h10.symm,
rw h10 at h3,
exact (domain.mul_left_inj (ne_of_lt hb0).symm).mp h3
end


This proof seems a bit long. Any suggestions for improving this?

#### Paul van Wamelen (Jun 21 2020 at 19:21):

All the haves are poor form also, right?

#### Yakov Pechersky (Jun 21 2020 at 19:33):

Shouldn't something like h10 : (((a : ℚ) / b).denom : ℤ) = b be a simp lemma as it is?

#### Paul van Wamelen (Jun 21 2020 at 19:44):

denom is the "canonical" denominator. That is, denom of (-2)/(-6) is 3.

#### Paul van Wamelen (Jun 21 2020 at 19:45):

This is slightly better:

lemma rat_id0 {a b : ℤ} (hb0 : 0 < b) (h : nat.coprime a.nat_abs b.nat_abs) :
a = ((a : ℚ) / b).num ∧ b = ((a : ℚ) / b).denom :=
begin
have h2 : (a : ℚ) / b = rat.mk ((a : ℚ) / b).num ((a : ℚ) / b).denom, { rw rat.num_denom },
rw ←rat.mk_eq_div at h2,
have h3 : a * ((a : ℚ) / b).denom = ((a : ℚ) / b).num * b,
{ apply (rat.mk_eq ((ne_of_lt hb0).symm) _).1,
{ rw h2, rw ←rat.mk_eq_div },
{ simp only [rat.denom_ne_zero, int.coe_nat_eq_zero, ne.def, not_false_iff] }},
have h4 : int.nat_abs b ∣ ((a : ℚ) / b).denom,
{ apply nat.coprime.dvd_of_dvd_mul_left (nat.coprime.symm h),
change b.nat_abs ∣ int.nat_abs a * int.nat_abs ((a : ℚ) / (b : ℚ)).denom,
rw ←int.nat_abs_mul, exact int.nat_abs_dvd_abs_iff.2 (dvd_of_mul_left_eq _ h3.symm) },
have h5 : ((a : ℚ) / b).denom ∣ int.nat_abs b,
{ apply nat.coprime.dvd_of_dvd_mul_left (nat.coprime.symm ((a : ℚ) / b).cop),
rw ←int.nat_abs_mul,
change int.nat_abs ((a : ℚ) / b).denom ∣ int.nat_abs (((a : ℚ) / b).num * b),
apply int.nat_abs_dvd_abs_iff.2,
apply dvd_of_mul_left_eq _ h3
},
have h6 : ((a : ℚ) / b).denom = int.nat_abs b, { exact nat.dvd_antisymm h5 h4 },
have h7 : (((a : ℚ) / b).denom : ℤ) = b,
{ rw [int.eq_nat_abs_of_zero_le (le_of_lt hb0)] {occs := occurrences.pos }, rw h6 },
apply and.intro _ h7.symm,
rw h7 at h3,
exact (domain.mul_left_inj (ne_of_lt hb0).symm).mp h3
end


#### Kenny Lau (Jun 21 2020 at 20:13):

import data.rat.basic tactic

lemma rat_id0 {a b : ℤ} (hb0 : 0 < b) (h : nat.coprime a.nat_abs b.nat_abs) :
(a / b : ℚ).num = a ∧ ((a / b : ℚ).denom : ℤ) = b :=
begin
lift b to ℕ using le_of_lt hb0,
norm_cast at hb0 h,
rw [← rat.mk_eq_div, ← rat.mk_pnat_eq a b hb0, rat.mk_pnat_num, rat.mk_pnat_denom,
pnat.mk_coe, h.gcd_eq_one, int.coe_nat_one, int.div_one, nat.div_one],
split; refl
end


#### Kenny Lau (Jun 21 2020 at 20:15):

using simp:

import data.rat.basic tactic

lemma rat_id0 {a b : ℤ} (hb0 : 0 < b) (h : nat.coprime a.nat_abs b.nat_abs) :
(a / b : ℚ).num = a ∧ ((a / b : ℚ).denom : ℤ) = b :=
begin
lift b to ℕ using le_of_lt hb0,
norm_cast at hb0 h,
rw [← rat.mk_eq_div, ← rat.mk_pnat_eq a b hb0],
split; simp [rat.mk_pnat_num, rat.mk_pnat_denom, h.gcd_eq_one]
end


#### Kenny Lau (Jun 21 2020 at 20:15):

(why aren't those simp lemmas?)

#### Paul van Wamelen (Jun 21 2020 at 20:29):

Ah, I missed rat.mk_pnat_num, and rat.mk_pnat_denom!

Last updated: May 11 2021 at 00:31 UTC