# Zulip Chat Archive

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

#### Chris Hughes (May 16 2020 at 17:08):

It's about characteristic n 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

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

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`

.

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

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

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

exactly

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

/me deletes all of his Lean repos other than mathlib

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

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

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

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,
nat.add_sub_cancel_left, nat.cast_add],
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,
nat.add_sub_cancel_left, nat.cast_add],
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,
nat.add_sub_cancel_left, nat.cast_add],
end
```

#### Johan Commelin (May 18 2020 at 14:03):

Hmm... thanks for keeping me honest.

#### Johan Commelin (May 18 2020 at 14:04):

It seems that my hardware is 3 times as fast... so I didn't really notice

Last updated: May 17 2021 at 15:13 UTC