## Stream: Is there code for X?

### Topic: eq_iff_modeq_int

#### Kevin Buzzard (May 16 2020 at 16:48):

lemma eq_iff_modeq_int {n : ℕ+} {a b : ℤ} : (a : zmod n) = b ↔ a ≡ b [ZMOD (n : ℕ)] := ...


I'm fixing up some old codewars kata and I find that this has disappeared from the library, in #2511. I need (a : zmod n) = b -> a % n = b % n. How am I supposed to get that now?

#### Kevin Buzzard (May 16 2020 at 17:14):

I need to learn about char_p?

#### Patrick Massot (May 16 2020 at 17:14):

No you don't, because you already learned it for the perfectoid project.

#### Kevin Buzzard (May 16 2020 at 17:22):

But n isn't prime!

#### Kevin Buzzard (May 16 2020 at 19:07):

lemma eq_iff_modeq_int {n : ℕ} {a b : ℤ} : (a : zmod n) = b ↔ a ≡ b [ZMOD (n : ℕ)] :=
by rw [eq_comm, ←sub_eq_zero, ←int.cast_sub, char_p.int_cast_eq_zero_iff (zmod n) n, int.modeq.modeq_iff_dvd]


#### Johan Commelin (May 16 2020 at 19:08):

But this doesn't use zmod n in an essential way, right?

#### Johan Commelin (May 16 2020 at 19:09):

So it should be a lemma about arbitrary R with char_p R n

#### Kevin Buzzard (May 16 2020 at 19:09):

All I care about is that my kata is compiling again right now

#### Mario Carneiro (May 16 2020 at 20:00):

@Johan Commelin you deleted a lemma? shame on you

#### Johan Commelin (May 16 2020 at 20:00):

Did I? Where? When?

#### Mario Carneiro (May 16 2020 at 20:01):

This was a lemma before the refactor, I can't find it now

Oops

#### Kevin Buzzard (May 16 2020 at 20:02):

eq_zero_iff_dvd_int got renamed to char_p.int_cast_eq_zero_iff and a similar story for nat, but the lemma in question just seemed to vanish completely.

#### Johan Commelin (May 16 2020 at 20:02):

I see... I guess I messed up with porting some of the zmodp stuff to zmod p.

My apologies

#### Kevin Buzzard (May 16 2020 at 20:03):

Johan is saying that we have a better lemma somewhere now

#### Johan Commelin (May 16 2020 at 20:03):

Hmm... except that maybe we don't have it...

#### Johan Commelin (May 16 2020 at 20:03):

I think I messed up

#### Johan Commelin (May 16 2020 at 20:06):

I will try to restore stuff next week... now I first need to rest.

#### Reid Barton (May 16 2020 at 20:07):

This is what you get for not PRing your katas to mathlib

exactly

#### Kevin Buzzard (May 16 2020 at 20:08):

/me deletes all of his Lean repos other than mathlib

Noooo!

#### Patrick Massot (May 16 2020 at 20:09):

Fortunately git is decentralized

#### Johan Commelin (May 16 2020 at 20:09):

The perfectoid repo is on the community account

#### Kevin Buzzard (May 17 2020 at 10:53):

Whilst proving example : (R : Type*) [ring R] (p : ℕ) [char_p R p] (a b : ℤ) : (a : R) = b ↔ a ≡ b [ZMOD p] I noticed the following thing:

theorem sub_eq_zero : a - b = 0 ↔ a = b


and

theorem modeq_iff_dvd : a ≡ b [ZMOD n] ↔ (n:ℤ) ∣ b - a


One a-b, one b-a. This meant that I had to add an eq_comm in the following proof:

import number_theory.quadratic_reciprocity
import data.int.modeq

lemma thing (R : Type*) [ring R] (p : ℕ) [char_p R p] (a b : ℤ) :
(a : R) = b ↔ a ≡ b [ZMOD p] :=
begin
rw eq_comm,
rw ←sub_eq_zero,
rw ←int.cast_sub,
rw char_p.int_cast_eq_zero_iff R p,
rw int.modeq.modeq_iff_dvd,
end


I think the above lemma is the correct thing to PR to mathlib (with perhaps a better proof) but this experience did make me wonder whether there should be a "convention" for the order of the subtractands when proving lemmas of this form.

#### Johan Commelin (May 18 2020 at 12:09):

I think the trouble with my refactor PR was that I completely rewrote the API for zmod. Hence a lot of auxilliary lemmas no longer made sense, or weren't needed. I guess this lemma was collateral damage. My apologies.
@Kevin Buzzard Do you want to PR it, or shall I do it?

#### Kevin Buzzard (May 18 2020 at 12:37):

I don't want to PR it, my PR's usually have to go through a few iterations and I am not looking at the mathlib github site at all at the minute

Ok, I'll do it.

#### Kevin Buzzard (May 18 2020 at 12:49):

Thanks. I'm trying to get another Lean post-doc and time is tight :-)

#### Johan Commelin (May 18 2020 at 13:33):

Is there a slick way of proving

import algebra.char_p
import data.int.modeq

lemma eq_iff_modeq (R : Type*) [semiring R] (p : ℕ) [char_p R p] (a b : ℕ) :
(a : R) = b ↔ a ≡ b [MOD p] :=
begin
wlog h : a ≤ b,
obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le h,
rw [nat.modeq.modeq_iff_dvd' h, ← char_p.cast_eq_zero_iff R p,
end


Currently I can only think of going through zmod p...

#### Kenny Lau (May 18 2020 at 13:35):

have we fixed wlog?

#### Johan Commelin (May 18 2020 at 13:37):

No, I don't think so.

#### Johan Commelin (May 18 2020 at 13:37):

But that's not the hard part (-;

#### Johan Commelin (May 18 2020 at 13:37):

I can easily work aroun wlog, of course

#### Johan Commelin (May 18 2020 at 13:37):

Note that in this particular case it isn't slow (for a human)

#### Kenny Lau (May 18 2020 at 13:44):

import algebra.char_p
import data.int.modeq

set_option profiler true

-- elaboration of eq_iff_modeq took 1.41s
lemma eq_iff_modeq (R : Type*) [semiring R] (p : ℕ) [char_p R p] (a b : ℕ) :
(a : R) = b ↔ a ≡ b [MOD p] :=
begin
wlog h : a ≤ b,
obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le h,
rw [nat.modeq.modeq_iff_dvd' h, ← char_p.cast_eq_zero_iff R p,
end

-- elaboration of eq_iff_modeq' took 222ms
lemma eq_iff_modeq' (R : Type*) [semiring R] (p : ℕ) [char_p R p] (a b : ℕ) :
(a : R) = b ↔ a ≡ b [MOD p] :=
begin
wlog h : a ≤ b := le_total a b using [a b, b a] tactic.skip,
swap, { rwa [eq_comm, nat.modeq, @eq_comm _ (a % p)] },
obtain ⟨k, rfl⟩ := nat.exists_eq_add_of_le h,
rw [nat.modeq.modeq_iff_dvd' h, ← char_p.cast_eq_zero_iff R p,
`