Zulip Chat Archive

Stream: new members

Topic: squares


view this post on Zulip Alex Kontorovich (Feb 10 2020 at 15:23):

Here's something trivial that I'm trying to formalize: If a and b are coprime and a*b is a perfect square, then a and b are squares.

def divides (x y : ) :=  d:, y=x*d

def coprime (x y :  ) :=  d: , (divides d x)  (divides d y) -> d=1

def is_square (x: ) :=  r:, x=r*r

lemma product_coprimes_square (a b c : ) (p: coprime a b) (p1 : a*b=c*c):
((is_square a)  (is_square b))
:= begin

end

The argument could go something like: a is a square <-> every prime in its factorization appears with even multiplicity. How does unique factorization work in Lean? Help please? Thanks!

view this post on Zulip Alex Kontorovich (Feb 10 2020 at 15:25):

Ooh stupid subtlety: a and b need to be positive, or else it's false!... (Originally I was doing this all in naturals, but elsewhere I need to subtract ... which doesn't exist for naturals!...)

view this post on Zulip Mario Carneiro (Feb 10 2020 at 15:27):

This is fine for an example, but if you want "real" theorems about primes and stuff then use the library definitions of divides and coprime (is_square doesn't have a definition)

view this post on Zulip Mario Carneiro (Feb 10 2020 at 15:28):

You can certainly subtract on naturals, but you have to do the subtraction in int if you want it to mean the expected thing

view this post on Zulip Mario Carneiro (Feb 10 2020 at 15:29):

Also your definition of divides isn't right for int, as it implies x and y have the same sign

view this post on Zulip Mario Carneiro (Feb 10 2020 at 15:30):

do you have mathlib?

view this post on Zulip Alex Kontorovich (Feb 10 2020 at 15:45):

yes I have mathlib. (How do I use it?...)

view this post on Zulip Alex Kontorovich (Feb 10 2020 at 15:48):

How do I fix this with "int" so that it works? (I can "cheat" and change \N to \Z...)

lemma converse (r s x y z:) (px: x= r*r-s*s) (py: y=2*r*s) (pz:z=r*r+s*s)
:
 x*x+y*y=z*z :=
begin
 rw px,
 rw py,
 rw pz,
 ring,
end

view this post on Zulip Alex Kontorovich (Feb 10 2020 at 15:49):

(the goal, if it isn't clear, is to show that, if x=r^2-s^2, y=2rs, and z=r^2+s^2, then x^2+y^2=z^2...)

view this post on Zulip Mario Carneiro (Feb 10 2020 at 15:57):

One option:

import tactic.ring
lemma converse (r s x y z:) (px: (x:) = r*r-s*s) (py: y=2*r*s) (pz:z=r*r+s*s) :
 x*x+y*y=z*z :=
begin
  apply int.coe_nat_inj,
  simp [px, py, pz],
  ring,
end

view this post on Zulip Reid Barton (Feb 10 2020 at 16:02):

There's a tricky way to prove your original statement avoiding prime factorization using prod_dvd_and_dvd_of_dvd_prod, which states (in particular) that if aa divides ccc*c, then a=dea = de with dd dividing cc and ee dividing cc.

view this post on Zulip Reid Barton (Feb 10 2020 at 16:03):

You might have fun working out the rest of the proof.

view this post on Zulip Reid Barton (Feb 10 2020 at 16:05):

(It's still kind of tricky after this step.)

view this post on Zulip Reid Barton (Feb 10 2020 at 16:06):

I have FLT for n=4 lying around on my old laptop, but it is for a 2 year old version of mathlib so it probably doesn't work any more.

view this post on Zulip Alex Kontorovich (Feb 10 2020 at 16:14):

Right, that's exactly where I'm going with this, FLT for n=4 (of course). Just to learn Lean. Thanks for the hint.

Related/complaint: I wish the file "prime.lean" used fever fancy tactics so mathematicians like me had less start-up cost...

view this post on Zulip Mario Carneiro (Feb 10 2020 at 16:14):

prime.lean uses very few fancy tactics last time I checked. In fact, that might be why it's not so readable

view this post on Zulip Alex Kontorovich (Feb 10 2020 at 16:27):

Heh :) As a mathematician who came here because Kevin made his "game" look very much like "regular math", the fewer tactics (besides, say, "ring", which for me means, leave the algebra as an exercise) the better (at least for me, for now).

view this post on Zulip Reid Barton (Feb 10 2020 at 16:28):

When I did this there was nothing in mathlib yet about prime factorization or multiplicity of primes so the easiest way was to use this little trick. But now we should be close to stating and proving things like if every exponent in the prime factorization of n is even, then n is a square, and of course these facts are more generally useful (or at least easiier to think of!)

view this post on Zulip Alex Kontorovich (Feb 10 2020 at 16:31):

Agreed! Is there a place where ord_p(n) is defined? (Exponent of p in the prime factorization of n)

view this post on Zulip Alex Kontorovich (Feb 10 2020 at 16:32):

I'm actually really curious in how the "descent" part of FLTn=4 will go. (Don't tell me yet... Still trying to get Pythagorean parametrization up and running)

view this post on Zulip Reid Barton (Feb 10 2020 at 16:35):

See multiplicity, in ring_theory.multiplicity

view this post on Zulip Alex Kontorovich (Feb 10 2020 at 16:36):

Thanks!


Last updated: May 08 2021 at 18:17 UTC