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

(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

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