Zulip Chat Archive

Stream: Is there code for X?

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


view this post on Zulip 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

view this post on Zulip Johan Commelin (Sep 08 2020 at 11:14):

Probably not

view this post on Zulip Ruben Van de Velde (Sep 08 2020 at 11:26):

is_pow_of_coprime from #3984, apparently

view this post on Zulip Reid Barton (Sep 08 2020 at 11:37):

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

view this post on Zulip Ruben Van de Velde (Sep 08 2020 at 11:38):

@Paul van Wamelen

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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