Zulip Chat Archive

Stream: new members

Topic: Proving a square isn't 2 mod 3


view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 05 2020 at 15:22):

Does that help?

view this post on Zulip 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

view this post on Zulip Johan Commelin (Nov 05 2020 at 15:22):

@Adrián Doña Mateo :up:

view this post on Zulip Reid Barton (Nov 05 2020 at 15:23):

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

view this post on Zulip Adrián Doña Mateo (Nov 05 2020 at 15:28):

Yes, I would like to reduce it to that

view this post on Zulip 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

view this post on Zulip 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