Zulip Chat Archive

Stream: maths

Topic: a*a = b*c -> gcd a b > 1


view this post on Zulip Rick Love (Aug 15 2020 at 14:12):

Good point, my final conclusion should be gcd a b > 1 (Corrected the title)

view this post on Zulip Rick Love (Aug 15 2020 at 14:14):

That also assumes a,b,c > 1

view this post on Zulip Rick Love (Aug 15 2020 at 14:18):

Ok, here is a better approach:

-- 4 * 4 = 2 * 8  -> gcd a b = 2 gcd a c = 4
-- 6 * 6 = 4 * 9  -> gcd a b = 2 gcd a c = 3
theorem multiple_factors_then_gcd (a b c k : nat):
    a > 1 -> b > 1 -> c > 1 ->
    a*a = b*c ->
    gcd a b > 1 :=
begin
    intros ha hb hc h,

    let faa := factors (a*a),
    let fbc := factors (b*c),
    let fa := factors (a),
    let fb := factors (b),
    let fc := factors (c),
    have h_faa_fbc : faa = fbc := by { dsimp [faa, fbc], rw h,},
    have h_faa_fa_fa : faa = list.append fa fa := by {
        -- cc,
        -- Is there an operation for factors(a*a) = factors(a) ∧ factors(a)
        sorry,
    },

    -- have
    sorry,

end

view this post on Zulip Kevin Buzzard (Aug 15 2020 at 14:22):

If all you want to do is prove the gcd is bigger than one then you can just prove that if b>1 then it has a prime factor and this prime factor divides a^2 and hence a

view this post on Zulip Kevin Buzzard (Aug 15 2020 at 14:22):

I should think these facts are already in mathlib

view this post on Zulip Rick Love (Aug 15 2020 at 14:25):

Right, I was trying to use dvd and gcd, but I'll take a look at the prime functions. That's probably the missing piece 'prime factor divides a^2 and hence a'

view this post on Zulip Kenny Lau (Aug 15 2020 at 17:19):

if gcd a b <= 1 then gcd a b = 0 or gcd a b = 1.

In the first case, we have a = 0 or b = 0, contradiction.

In the second case, we have gcd (a * a) b = 1, so gcd (b * c) b = 1, so b = 1, contradiction.

view this post on Zulip Kenny Lau (Aug 15 2020 at 17:19):

no primes required

view this post on Zulip Rick Love (Aug 15 2020 at 17:38):

@Kenny Lau even with that, the difficulty is programming it in lean. How would you write that? Specifically how would you set up a proof by contradiction like this. (Note, I've done plenty of rw apply, etc, but still new to using exfalso and a contradiction).

view this post on Zulip Kenny Lau (Aug 15 2020 at 17:47):

you can start with:

  generalize hg : gcd a b = g,
  by_contra h,
  cases g with g,

(not tested)

view this post on Zulip Rick Love (Aug 15 2020 at 17:54):

Well that's giving me:
image.png

How do I pull the h out to work with it?

view this post on Zulip Johan Commelin (Aug 15 2020 at 17:59):

What do you mean with "pull out"? Does push_neg help?

view this post on Zulip Kenny Lau (Aug 15 2020 at 17:59):

what's your goal state before my invocations?

view this post on Zulip Rick Love (Aug 15 2020 at 19:52):

Johan Commelin said:

What do you mean with "pull out"? Does push_neg help?

Yeah, that helps. I'd just been using simp, but this gives better control.


Last updated: May 11 2021 at 16:22 UTC