feat(algebra/char_p): eq_iff_modeq_int (#2731)

src/algebra/char_p.lean

@@ -8,6 +8,7 @@ Characteristic of semirings.
 
 import data.fintype.basic
 import data.nat.choose
+import data.int.modeq
 import algebra.module
 
 universes u v
@@ -84,6 +85,11 @@ begin
   rw [pow_zero, nat.sub_zero, one_mul, nat.choose_zero_right, nat.cast_one, mul_one]
 end
 
+lemma eq_iff_modeq_int (R : Type*) [ring R] (p : ℕ) [char_p R p] (a b : ℤ) :
+  (a : R) = b ↔ 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]
+
 section frobenius
 
 variables (R : Type u) [comm_ring R] {S : Type v} [comm_ring S] (f : R →* S) (g : R →+* S)