Congruence modulo multiples and congruence modulo AddSubgroup.zmultiples _

In this file we show that in an additive commutative group, the congruence relation a ≡ b [PMOD p] is equivalent to the coercions of a and b to G ⧸ AddSubgroup.zmultiples p being equal.

theorem AddCommGroup.modEq_iff_eq_mod_zmultiples {G : Type u_1} [AddCommGroup G] {a b p : G} : a ≡ b [PMOD p] ↔ ↑a = ↑b

theorem AddCommGroup.not_modEq_iff_ne_mod_zmultiples {G : Type u_1} [AddCommGroup G] {a b p : G} : ¬a ≡ b [PMOD p] ↔ ↑a ≠ ↑b