# Zulip Chat Archive

## Stream: Is there code for X?

### Topic: zmod

#### Scott Morrison (May 23 2020 at 10:25):

I'm failing to find two of the most basic facts about `zmod`

:

```
example (a b c : ℕ) (h : (a : zmod c) = (b : zmod c)) : a % c = b % c :=
sorry
example (a b : ℕ) (h : (a : zmod b) = 0) : b ∣ a :=
sorry
```

and worse, I don't seem to be able to prove them... Any help?

#### Scott Morrison (May 23 2020 at 10:28):

Actually, I guess it's actually the other direction I want in any case.

#### Kevin Buzzard (May 23 2020 at 10:28):

You want to look at `modeq`

#### Kevin Buzzard (May 23 2020 at 10:28):

That's the language the lemmas are proved in

#### Patrick Massot (May 23 2020 at 10:29):

(deleted)

#### Scott Morrison (May 23 2020 at 10:30):

But I don't want to use `modeq`

, because it is horrible. :-) I am working with (Z/NZ) + \sqrt{3} (Z/NZ).

#### Scott Morrison (May 23 2020 at 10:31):

It seems like the coercion from `nat`

to `zmod`

isn't particularly well described in the API, so it's hard to extract information from hypotheses about these coercions.

#### Kevin Buzzard (May 23 2020 at 10:32):

I posted a proof of one of these the other day

#### Kevin Buzzard (May 23 2020 at 10:33):

I'm on mobile and don't know how to send the link but search for

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

#### Scott Morrison (May 23 2020 at 10:34):

Okay, that lemma does look good.

#### Scott Morrison (May 23 2020 at 10:34):

It never made it into mathlib?

#### Kevin Buzzard (May 23 2020 at 10:35):

I certainly didn't PR it. My life is too full right now, I would PR, get a comment, and then not notice for two weeks and this is a bit annoying

#### Scott Morrison (May 23 2020 at 10:35):

I guess I still need to adapt it for the nat version instead of int.

#### Scott Morrison (May 23 2020 at 10:35):

okay, I'll see if I can include something like it

#### Kevin Buzzard (May 23 2020 at 10:36):

Unfortunately I use subtraction

#### Kevin Buzzard (May 23 2020 at 10:36):

Maybe you can start with WLOG

#### Scott Morrison (May 23 2020 at 10:48):

Okay,

```
lemma char_p.int_coe_eq_int_coe_iff (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
lemma zmod.int_coe_eq_int_coe_iff (a b : ℤ) (c : ℕ) : (a : zmod c) = (b : zmod c) ↔ a ≡ b [ZMOD c] :=
char_p.int_coe_eq_int_coe_iff (zmod c) c a b
lemma zmod.nat_coe_eq_nat_coe_iff (a b c : ℕ) : (a : zmod c) = (b : zmod c) ↔ a ≡ b [MOD c] :=
begin
convert zmod.int_coe_eq_int_coe_iff a b c,
simp [nat.modeq.modeq_iff_dvd, int.modeq.modeq_iff_dvd],
end
@[simp]
lemma coe_zmod_eq_zero_iff_dvd (a b : ℕ) : (a : zmod b) = 0 ↔ b ∣ a :=
begin
change (a : zmod b) = ((0 : ℕ) : zmod b) ↔ b ∣ a,
rw zmod.nat_coe_eq_nat_coe_iff,
rw nat.modeq.modeq_zero_iff,
end
```

starts with Kevin's lemma and deduces what I needed. (No need for wlog!). I'll bundle it all into an upcoming PR.

#### Shing Tak Lam (May 23 2020 at 11:03):

Here's a direct proof of your original examples?

```
import data.zmod.basic
example (a b c : ℕ) (h : (a : zmod c) = (b : zmod c)) : a % c = b % c :=
by rw [←zmod.val_cast_nat, ←zmod.val_cast_nat, h]
example (a b : ℕ) (h : (a : zmod b) = 0) : b ∣ a :=
by rw [nat.dvd_iff_mod_eq_zero, ←zmod.val_cast_nat, h, zmod.val_zero]
```

#### Patrick Massot (May 23 2020 at 11:12):

Could you please try to use `norm_cast`

in all those proofs? Each proof that requires adding a `norm_cast`

attribute benefits to future users beyond its intended use.

#### Johan Commelin (May 23 2020 at 14:36):

@Scott Morrison mathlib knows `char_p (zmod n) n`

, and your questions ought to be proven for a general such `R`

.

#### Johan Commelin (May 23 2020 at 14:39):

The second one is (half of) the definition of `char_p`

:

```
example (a b : ℕ) (h : (a : zmod b) = 0) : b ∣ a :=
(char_p.cast_eq_zero_iff (zmod b) b a).mp h
```

Last updated: May 17 2021 at 16:26 UTC