squares

Stream: new members

[Alex Kontorovich]

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]

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]

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]

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]

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

[Mario Carneiro]

do you have mathlib?

[Alex Kontorovich]

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

[Alex Kontorovich]

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]

(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]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Alex Kontorovich]

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]

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]

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

[Alex Kontorovich]

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]

See multiplicity, in ring_theory.multiplicity

[Alex Kontorovich]

Thanks!