chore(Algebra/ModEq): split file (leanprover-community#34003)

Minor modifications to the lemmas linking it to `Nat.ModEq` and
`Int.ModEq` to make the proofs work, otherwise copy+paste+add stub
module docs.

Author: urkud

Mathlib.lean

@@ -296,6 +296,7 @@ public import Mathlib.Algebra.Field.Equiv
 public import Mathlib.Algebra.Field.GeomSum
 public import Mathlib.Algebra.Field.IsField
 public import Mathlib.Algebra.Field.MinimalAxioms
+public import Mathlib.Algebra.Field.ModEq
 public import Mathlib.Algebra.Field.NegOnePow
 public import Mathlib.Algebra.Field.Opposite
 public import Mathlib.Algebra.Field.Periodic
@@ -391,6 +392,7 @@ public import Mathlib.Algebra.Group.Irreducible.Defs
 public import Mathlib.Algebra.Group.Irreducible.Indecomposable
 public import Mathlib.Algebra.Group.Irreducible.Lemmas
 public import Mathlib.Algebra.Group.MinimalAxioms
+public import Mathlib.Algebra.Group.ModEq
 public import Mathlib.Algebra.Group.Nat.Defs
 public import Mathlib.Algebra.Group.Nat.Even
 public import Mathlib.Algebra.Group.Nat.Hom
@@ -4426,6 +4428,7 @@ public import Mathlib.GroupTheory.PushoutI
 public import Mathlib.GroupTheory.QuotientGroup.Basic
 public import Mathlib.GroupTheory.QuotientGroup.Defs
 public import Mathlib.GroupTheory.QuotientGroup.Finite
+public import Mathlib.GroupTheory.QuotientGroup.ModEq
 public import Mathlib.GroupTheory.Rank
 public import Mathlib.GroupTheory.RegularWreathProduct
 public import Mathlib.GroupTheory.Schreier

Mathlib/Algebra/Field/ModEq.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2023 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+module
+
+public import Mathlib.Algebra.Group.ModEq
+public import Mathlib.Algebra.Field.Basic
+public import Mathlib.Tactic.MinImports
+
+/-!
+# Congruence modulo multiples of an element in a (semi)field
+
+In this file we prove a few theorems about the congruence relation `_ ≡ _ [PMOD _]`
+in a division semiring or a semifield.
+-/
+
+public section
+
+namespace AddCommGroup
+
+section DivisionSemiring
+variable {K : Type*} [DivisionSemiring K] {a b c p : K}
+
+@[simp] lemma div_modEq_div (hc : c ≠ 0) : a / c ≡ b / c [PMOD p] ↔ a ≡ b [PMOD (p * c)] := by
+  simp [modEq_iff_nsmul, add_div' _ _ _ hc, div_left_inj' hc, mul_assoc]
+
+@[simp] lemma mul_modEq_mul_right (hc : c ≠ 0) : a * c ≡ b * c [PMOD p] ↔ a ≡ b [PMOD (p / c)] := by
+  rw [div_eq_mul_inv, ← div_modEq_div (inv_ne_zero hc), div_inv_eq_mul, div_inv_eq_mul]
+
+end DivisionSemiring
+
+section Semifield
+variable {K : Type*} [Semifield K] {a b c p : K}
+
+@[simp] lemma mul_modEq_mul_left (hc : c ≠ 0) : c * a ≡ c * b [PMOD p] ↔ a ≡ b [PMOD (p / c)] := by
+  simp [mul_comm c, hc]
+
+end Semifield
+end AddCommGroup