doc(int/modeq): add module doc and tidy (#7878)

Author: ericrbg

src/data/int/modeq.lean

@@ -6,9 +6,24 @@ Authors: Chris Hughes
 import data.nat.modeq
 import tactic.ring
 
+/-!
+
+# Congruences modulo an integer
+
+This file defines the equivalence relation `a ≡ b [ZMOD n]` on the integers, similarly to how
+`data.nat.modeq` defines them for the natural numbers. The notation is short for `modeq a b n`,
+which is defined to be `a % n = b % n` for integer `a b n`.
+
+## Tags
+
+modeq, congruence, mod, MOD, modulo, integers
+
+-/
+
 namespace int
 
 /-- `a ≡ b [ZMOD n]` when `a % n = b % n`. -/
+@[derive decidable]
 def modeq (n a b : ℤ) := a % n = b % n
 
 notation a ` ≡ `:50 b ` [ZMOD `:50 n `]`:0 := modeq n a b
@@ -25,8 +40,6 @@ variables {n m a b c d : ℤ}
 lemma coe_nat_modeq_iff {a b n : ℕ} : a ≡ b [ZMOD n] ↔ a ≡ b [MOD n] :=
 by unfold modeq nat.modeq; rw ← int.coe_nat_eq_coe_nat_iff; simp [int.coe_nat_mod]
 
-instance : decidable (a ≡ b [ZMOD n]) := by unfold modeq; apply_instance
-
 theorem modeq_zero_iff : a ≡ 0 [ZMOD n] ↔ n ∣ a :=
 by rw [modeq, zero_mod, dvd_iff_mod_eq_zero]
 
@@ -106,10 +119,9 @@ calc a + n*c ≡ b + n*c [ZMOD n] : int.modeq.modeq_add ha (int.modeq.refl _)
                  (int.modeq.modeq_zero_iff.2 (dvd_mul_right _ _))
          ... ≡ b [ZMOD n] : by simp
 
-open nat
-lemma mod_coprime {a b : ℕ} (hab : coprime a b) : ∃ y : ℤ, a * y ≡ 1 [ZMOD b] :=
+lemma mod_coprime {a b : ℕ} (hab : nat.coprime a b) : ∃ y : ℤ, a * y ≡ 1 [ZMOD b] :=
 ⟨ nat.gcd_a a b,
-  have hgcd : nat.gcd a b = 1, from coprime.gcd_eq_one hab,
+  have hgcd : nat.gcd a b = 1, from nat.coprime.gcd_eq_one hab,
   calc
    ↑a * nat.gcd_a a b ≡ ↑a * nat.gcd_a a b + ↑b * nat.gcd_b a b [ZMOD ↑b] : int.modeq.symm $
                       modeq_add_fac _ $ int.modeq.refl _