# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: Coprime numbers whose product is a square are both square

#### Ruben Van de Velde (Sep 08 2020 at 11:04):

lemma coprime_sq (a b c : ℤ) (h : a * b = c ^ 2) (hcoprime : is_coprime a b) :

∃ d e, a = d ^ 2 ∧ b = e ^ 2 := sorry

#### Johan Commelin (Sep 08 2020 at 11:14):

Probably not

#### Ruben Van de Velde (Sep 08 2020 at 11:26):

is_pow_of_coprime from #3984, apparently

#### Reid Barton (Sep 08 2020 at 11:37):

Oh that reminds me, let me dig up my old FLT code

#### Ruben Van de Velde (Sep 08 2020 at 11:38):

@Paul van Wamelen

#### Reid Barton (Sep 08 2020 at 11:48):

Well, I think it predates elan so I don't really know how to build it (apparently I used to build it with a version of lean called "3.3.1"), but I put it up at https://github.com/rwbarton/lean-elementary-number-theory

#### Reid Barton (Sep 08 2020 at 12:02):

in particular, the statement about multiplying to a square is at https://github.com/rwbarton/lean-elementary-number-theory/blob/master/src/ent/gcd.lean#L60-L61 -- it doesn't actually need prime factorization, you can get it from docs#nat.prod_dvd_and_dvd_of_dvd_prod, though I made it look quite difficult

#### Paul van Wamelen (Sep 08 2020 at 16:13):

PR #4049 has:

```
theorem is_pow_of_coprime {a b c : associates α} (ha : a ≠ 0) (hb : b ≠ 0)
(hab : ∀ d, d ∣ a → d ∣ b → ¬ prime d) {k : ℕ} (h : a * b = c ^ k)
: ∃ (d : associates α), a = d ^ k
```

for `α`

a unique factorization domain. From there it isn't too hard to get to:

```
lemma sqr_of_coprime {a b c : ℤ} (hc : c ≠ 0) (h : int.gcd a b = 1) (heq : a * b = c ^ 2) :
∃ (a0 : ℤ), a0 ≠ 0 ∧ (a = a0 ^ 2 ∨ a = - (a0 ^ 2))
```

(but this hasn't been PR'd yet). Let me know if you want the code...

Last updated: May 17 2021 at 14:12 UTC