## Stream: new members

### Topic: Proving a square isn't 2 mod 3

#### Adrián Doña Mateo (Nov 05 2020 at 15:16):

Is there an easy way to prove this?

import data.nat.modeq

/-- A square is not congruent to 2 module 3 -/
lemma not_square_of_two_mod_three (n : ℕ) (h : n ≡ 2 [MOD 3]) :
¬∃ m, m * m = n := sorry


My initial plan was to show that (m : zmod 3) * ↑m = ↑2 and then use fin_cases on ↑m to find a contradiction, but I can't seem to prove this first statement. I would want to use something like a * b = c → ↑a * ↑b = ↑c but I can't find this anywhere.

#### Johan Commelin (Nov 05 2020 at 15:22):

import data.nat.modeq
import data.zmod.basic

/-- A square is not congruent to 2 module 3 -/
lemma not_square_of_two_mod_three :
¬∃ (m : zmod 3), m * m = 2 := dec_trivial


Does that help?

#### Johan Commelin (Nov 05 2020 at 15:22):

The benefit of using zmod is that it is a finite type, so lean can just prove everything without your help

#### Reid Barton (Nov 05 2020 at 15:23):

I think the question is how to reduce the original statement to this one

#### Adrián Doña Mateo (Nov 05 2020 at 15:28):

Yes, I would like to reduce it to that

#### Shing Tak Lam (Nov 05 2020 at 15:32):

import data.nat.modeq
import data.zmod.basic
import data.nat.modeq

/-- A square is not congruent to 2 module 3 -/
lemma not_square_of_two_mod_three :
¬∃ (m : zmod 3), m * m = 2 := dec_trivial

/-- A square is not congruent to 2 module 3 -/
lemma not_square_of_two_mod_three' (n : ℕ) (h : n ≡ 2 [MOD 3]) :
¬∃ m, m * m = n :=
begin
rintro ⟨m, rfl⟩,
apply not_square_of_two_mod_three,
use m,
norm_cast,
rwa ←zmod.eq_iff_modeq_nat at h,
end


#### Adrián Doña Mateo (Nov 05 2020 at 15:36):

I see, so norm_cast was the piece I was missing. Thank you! These are very nice solutions.

Last updated: May 13 2021 at 21:12 UTC