feat(data/zmod/basic): simp lemmas for zmod

src/data/zmod/basic.lean

@@ -115,6 +115,9 @@ by rw [val_cast_nat, nat.mod_eq_of_lt h]
 @[simp] lemma cast_mod_nat (n : ℕ+) (a : ℕ) : ((a % n : ℕ) : zmod n) = a :=
 by conv {to_rhs, rw ← nat.mod_add_div a n}; simp
 
+@[simp] lemma cast_mod_nat' {n : ℕ} (hn : 0 < n) (a : ℕ) : ((a % n : ℕ) : zmod ⟨n, hn⟩) = a :=
+cast_mod_nat _ _
+
 @[simp] lemma cast_val {n : ℕ+} (a : zmod n) : (a.val : zmod n) = a :=
 by cases a; simp [mk_eq_cast]
 
@@ -140,6 +143,9 @@ lemma eq_iff_modeq_nat {n : ℕ+} {a b : ℕ} : (a : zmod n) = b ↔ a ≡ b [MO
   rwa [val_cast_nat, val_cast_nat] at this,
 λ h, fin.eq_of_veq $ by rwa [val_cast_nat, val_cast_nat]⟩
 
+lemma eq_iff_modeq_nat' {n : ℕ} (hn : 0 < n) {a b : ℕ} : (a : zmod ⟨n, hn⟩) = b ↔ a ≡ b [MOD n] :=
+eq_iff_modeq_nat
+
 lemma eq_iff_modeq_int {n : ℕ+} {a b : ℤ} : (a : zmod n) = b ↔ a ≡ b [ZMOD (n : ℕ)] :=
 ⟨λ h, by have := fin.veq_of_eq h;
   rwa [val_cast_int, val_cast_int, ← int.coe_nat_eq_coe_nat_iff,
@@ -148,6 +154,9 @@ lemma eq_iff_modeq_int {n : ℕ+} {a b : ℤ} : (a : zmod n) = b ↔ a ≡ b [ZM
 λ h : a % (n : ℕ) = b % (n : ℕ),
   by rw [← cast_mod_int n a, ← cast_mod_int n b, h]⟩
 
+lemma eq_iff_modeq_int' {n : ℕ} (hn : 0 < n) {a b : ℤ} :
+  (a : zmod ⟨n, hn⟩) = b ↔ a ≡ b [ZMOD (n : ℕ)] := eq_iff_modeq_int
+
 lemma eq_zero_iff_dvd_nat {n : ℕ+} {a : ℕ} : (a : zmod n) = 0 ↔ (n : ℕ) ∣ a :=
 by rw [← @nat.cast_zero (zmod n), eq_iff_modeq_nat, nat.modeq.modeq_zero_iff]
 
@@ -322,4 +331,4 @@ instance : discrete_field (zmodp p hp) :=
   ..zmodp.comm_ring hp,
   ..zmodp.has_inv hp }
 
-end zmodp
+end zmodp