feat(data/zmod): lemmas about coercions to zmod (#2802)

I'm not particularly happy with the location of these new lemmas within the file `data.zmod`. If anyone has a suggestion that they should be some particular place higher or lower in the file, that would be welcome.

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/char_p.lean

@@ -32,6 +32,11 @@ begin
     rw [int.cast_coe_nat, char_p.cast_eq_zero_iff R p, int.coe_nat_dvd] }
 end
 
+lemma char_p.int_coe_eq_int_coe_iff (R : Type*) [ring R] (p : ℕ) [char_p R p] (a b : ℤ) :
+  (a : R) = (b : R) ↔ a ≡ b [ZMOD p] :=
+by rw [eq_comm, ←sub_eq_zero, ←int.cast_sub,
+       char_p.int_cast_eq_zero_iff R p, int.modeq.modeq_iff_dvd]
+
 theorem char_p.eq (α : Type u) [semiring α] {p q : ℕ} (c1 : char_p α p) (c2 : char_p α q) : p = q :=
 nat.dvd_antisymm
   ((char_p.cast_eq_zero_iff α p q).1 (char_p.cast_eq_zero _ _))

src/data/zmod/basic.lean

@@ -331,6 +331,36 @@ lemma cast_int_cast (k : ℤ) : ((k : zmod n) : R) = k :=
 
 end universal_property
 
+lemma 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 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
+
+lemma int_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.int_coe_eq_int_coe_iff, int.modeq.modeq_zero_iff],
+end
+
+lemma nat_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, nat.modeq.modeq_zero_iff],
+end
+
+@[push_cast]
+lemma cast_mod_int (a : ℤ) (b : ℕ) : ((a % b : ℤ) : zmod b) = (a : zmod b) :=
+begin
+  rw zmod.int_coe_eq_int_coe_iff,
+  apply int.modeq.mod_modeq,
+end
+
 lemma val_injective (n : ℕ) [fact (0 < n)] :
   function.injective (zmod.val : zmod n → ℕ) :=
 begin