Coprime numbers whose product is a square are both square

Stream: Is there code for X?

[Ruben Van de Velde]

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]

Probably not

[Ruben Van de Velde]

is_pow_of_coprime from #3984, apparently

[Reid Barton]

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

[Ruben Van de Velde]

@Paul van Wamelen

[Reid Barton]

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]

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]

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...