## Stream: new members

### Topic: squares

#### 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!

#### 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!...)

#### 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)

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

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

#### Mario Carneiro (Feb 10 2020 at 15:30):

do you have mathlib?

#### Alex Kontorovich (Feb 10 2020 at 15:45):

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

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


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

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


#### 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 $a$ divides $c*c$, then $a = de$ with $d$ dividing $c$ and $e$ dividing $c$.

#### Reid Barton (Feb 10 2020 at 16:03):

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

#### Reid Barton (Feb 10 2020 at 16:05):

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

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

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

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

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

#### 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!)

#### 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)

#### 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)

#### Reid Barton (Feb 10 2020 at 16:35):

See multiplicity, in ring_theory.multiplicity

#### Alex Kontorovich (Feb 10 2020 at 16:36):

Thanks!

Last updated: May 08 2021 at 18:17 UTC