refactor(algebra): Redefine a ≡ b [PMOD p] (#18958)

YaelDillies · eric-wieser · YaelDillies · commit a07d750983b9 · 2023-05-10T11:33:42.000Z
as `∃ n : ℤ, b - a = n • p` instead of `∀ n : ℤ, b - n • p ∉ set.Ioo a (a + p)`. Since this new definition doesn't require an order on `α`, we move it to a new file `algebra.modeq`. Expand the API.



Co-authored-by: Eric Wieser &lt;wieser.eric@gmail.com&gt;
diff --git a/src/algebra/group/basic.lean b/src/algebra/group/basic.lean
@@ -451,6 +451,9 @@ by rw [div_eq_mul_inv, mul_right_inv a]
 lemma mul_div_cancel'' (a b : G) : a * b / b = a :=
 by rw [div_eq_mul_inv, mul_inv_cancel_right a b]
 
+@[simp, to_additive sub_add_cancel'']
+lemma div_mul_cancel''' (a b : G) : a / (b * a) = b⁻¹ := by rw [←inv_div, mul_div_cancel'']
+
 @[simp, to_additive]
 lemma mul_div_mul_right_eq_div (a b c : G) : (a * c) / (b * c) = a / b :=
 by rw [div_mul_eq_div_div_swap]; simp only [mul_left_inj, eq_self_iff_true, mul_div_cancel'']
diff --git a/src/algebra/group_power/lemmas.lean b/src/algebra/group_power/lemmas.lean
@@ -423,6 +423,11 @@ by { dsimp [bit1], rw [add_mul, bit0_mul, one_mul], }
 lemma mul_bit1 [non_assoc_ring R] {n r : R} : r * bit1 n = (2 : ℤ) • (r * n) + r :=
 by { dsimp [bit1], rw [mul_add, mul_bit0, mul_one], }
 
+/-- Note this holds in marginally more generality than `int.cast_mul` -/
+lemma int.cast_mul_eq_zsmul_cast [add_comm_group_with_one α] : ∀ m n, ((m * n : ℤ) : α) = m • n :=
+λ m, int.induction_on' m 0 (by simp) (λ k _ ih n, by simp [add_mul, add_zsmul, ih])
+  (λ k _ ih n, by simp [sub_mul, sub_zsmul, ih, ←sub_eq_add_neg])
+
 @[simp] theorem zsmul_eq_mul [ring R] (a : R) : ∀ (n : ℤ), n • a = n * a
 | (n : ℕ) := by rw [coe_nat_zsmul, nsmul_eq_mul, int.cast_coe_nat]
 | -[1+ n] := by simp [nat.cast_succ, neg_add_rev, int.cast_neg_succ_of_nat, add_mul]
diff --git a/src/algebra/hom/units.lean b/src/algebra/hom/units.lean
@@ -278,7 +278,9 @@ h.eq_div_iff.2
 @[to_additive] protected lemma div_eq_one_iff_eq (h : is_unit b) : a / b = 1 ↔ a = b :=
 ⟨eq_of_div_eq_one, λ hab, hab.symm ▸ h.div_self⟩
 
-@[to_additive] protected lemma div_mul_left (h : is_unit b) : b / (a * b) = 1 / a :=
+/-- The `group` version of this lemma is `div_mul_cancel'''` -/ 
+@[to_additive "The `add_group` version of this lemma is `sub_add_cancel''`"]
+protected lemma div_mul_left (h : is_unit b) : b / (a * b) = 1 / a :=
 by rw [div_eq_mul_inv, mul_inv_rev, h.mul_inv_cancel_left, one_div]
 
 @[to_additive] protected lemma mul_div_mul_right (h : is_unit c) (a b : α) :
diff --git a/src/algebra/modeq.lean b/src/algebra/modeq.lean
@@ -0,0 +1,219 @@
+/-
+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
+-/
+import data.int.modeq
+import group_theory.quotient_group
+
+/-!
+# Equality modulo an element
+
+This file defines equality modulo an element in a commutative group.
+
+## Main definitions
+
+* `a ≡ b [PMOD p]`: `a` and `b` are congruent modulo a`p`.
+
+## See also
+
+`smodeq` is a generalisation to arbitrary submodules.
+
+## TODO
+
+Delete `int.modeq` in favour of `add_comm_group.modeq`. Generalise `smodeq` to `add_subgroup` and
+redefine `add_comm_group.modeq` using it. Once this is done, we can rename `add_comm_group.modeq`
+to `add_subgroup.modeq` and multiplicativise it. Longer term, we could generalise to submonoids and
+also unify with `nat.modeq`.
+-/
+
+namespace add_comm_group
+variables {α : Type*}
+
+section add_comm_group
+variables [add_comm_group α] {p a a₁ a₂ b b₁ b₂ c : α} {n : ℕ} {z : ℤ}
+
+/-- `a ≡ b [PMOD p]` means that `b` is congruent to `a` modulo `p`.
+
+Equivalently (as shown in `algebra.order.to_interval_mod`), `b` does not lie in the open interval
+`(a, a + p)` modulo `p`, or `to_Ico_mod hp a` disagrees with `to_Ioc_mod hp a` at `b`, or
+`to_Ico_div hp a` disagrees with `to_Ioc_div hp a` at `b`. -/
+def modeq (p a b : α) : Prop := ∃ z : ℤ, b - a = z • p
+
+notation a ` ≡ `:50 b ` [PMOD `:50 p `]`:0 := modeq p a b
+
+@[refl, simp] lemma modeq_refl (a : α) : a ≡ a [PMOD p] := ⟨0, by simp⟩
+
+lemma modeq_rfl : a ≡ a [PMOD p] := modeq_refl _
+
+lemma modeq_comm : a ≡ b [PMOD p] ↔ b ≡ a [PMOD p] :=
+(equiv.neg _).exists_congr_left.trans $ by simp [modeq, ←neg_eq_iff_eq_neg]
+
+alias modeq_comm ↔ modeq.symm _
+
+attribute [symm] modeq.symm
+
+@[trans] lemma modeq.trans : a ≡ b [PMOD p] → b ≡ c [PMOD p] → a ≡ c [PMOD p] :=
+λ ⟨m, hm⟩ ⟨n, hn⟩, ⟨m + n, by simp [add_smul, ←hm, ←hn]⟩
+
+instance : is_refl _ (modeq p) := ⟨modeq_refl⟩
+
+@[simp] lemma neg_modeq_neg : -a ≡ -b [PMOD p] ↔ a ≡ b [PMOD p] :=
+modeq_comm.trans $ by simp [modeq]
+
+alias neg_modeq_neg ↔ modeq.of_neg modeq.neg
+
+@[simp] lemma modeq_neg : a ≡ b [PMOD -p] ↔ a ≡ b [PMOD p] :=
+modeq_comm.trans $ by simp [modeq, ←neg_eq_iff_eq_neg]
+
+alias modeq_neg ↔ modeq.of_neg' modeq.neg'
+
+lemma modeq_sub (a b : α) : a ≡ b [PMOD b - a] := ⟨1, (one_smul _ _).symm⟩
+
+@[simp] lemma modeq_zero : a ≡ b [PMOD 0] ↔ a = b := by simp [modeq, sub_eq_zero, eq_comm]
+
+@[simp] lemma self_modeq_zero : p ≡ 0 [PMOD p] := ⟨-1, by simp⟩
+
+@[simp] lemma zsmul_modeq_zero (z : ℤ) : z • p ≡ 0 [PMOD p] := ⟨-z, by simp⟩
+lemma add_zsmul_modeq (z : ℤ) : a + z • p ≡ a [PMOD p] := ⟨-z, by simp⟩
+lemma zsmul_add_modeq (z : ℤ) : z • p + a ≡ a [PMOD p] := ⟨-z, by simp⟩
+lemma add_nsmul_modeq (n : ℕ) : a + n • p ≡ a [PMOD p] := ⟨-n, by simp⟩
+lemma nsmul_add_modeq (n : ℕ) : n • p + a ≡ a [PMOD p] := ⟨-n, by simp⟩
+
+namespace modeq
+
+protected lemma add_zsmul (z : ℤ) : a ≡ b [PMOD p] → a + z • p ≡ b [PMOD p] :=
+(add_zsmul_modeq _).trans
+protected lemma zsmul_add (z : ℤ) : a ≡ b [PMOD p] → z • p + a ≡ b [PMOD p] :=
+(zsmul_add_modeq _).trans
+protected lemma add_nsmul (n : ℕ) : a ≡ b [PMOD p] → a + n • p ≡ b [PMOD p] :=
+(add_nsmul_modeq _).trans
+protected lemma nsmul_add (n : ℕ) : a ≡ b [PMOD p] → n • p + a ≡ b [PMOD p] :=
+(nsmul_add_modeq _).trans
+
+protected lemma of_zsmul : a ≡ b [PMOD (z • p)] → a ≡ b [PMOD p] :=
+λ ⟨m, hm⟩, ⟨m * z, by rwa [mul_smul]⟩
+
+protected lemma of_nsmul : a ≡ b [PMOD (n • p)] → a ≡ b [PMOD p] :=
+λ ⟨m, hm⟩, ⟨m * n, by rwa [mul_smul, coe_nat_zsmul]⟩
+
+protected lemma zsmul : a ≡ b [PMOD p] → z • a ≡ z • b [PMOD (z • p)] :=
+Exists.imp $ λ m hm, by rw [←smul_sub, hm, smul_comm]
+
+protected lemma nsmul : a ≡ b [PMOD p] → n • a ≡ n • b [PMOD (n • p)] :=
+Exists.imp $ λ m hm, by rw [←smul_sub, hm, smul_comm]
+
+end modeq
+
+@[simp] lemma zsmul_modeq_zsmul [no_zero_smul_divisors ℤ α] (hn : z ≠ 0) :
+  z • a ≡ z • b [PMOD (z • p)] ↔ a ≡ b [PMOD p] :=
+exists_congr $ λ m, by rw [←smul_sub, smul_comm, smul_right_inj hn]; apply_instance
+
+@[simp] lemma nsmul_modeq_nsmul [no_zero_smul_divisors ℕ α] (hn : n ≠ 0) :
+  n • a ≡ n • b [PMOD (n • p)] ↔ a ≡ b [PMOD p] :=
+exists_congr $ λ m, by rw [←smul_sub, smul_comm, smul_right_inj hn]; apply_instance
+
+alias zsmul_modeq_zsmul ↔ modeq.zsmul_cancel _
+alias nsmul_modeq_nsmul ↔ modeq.nsmul_cancel _
+
+namespace modeq
+
+@[simp] protected lemma add_iff_left :
+  a₁ ≡ b₁ [PMOD p] → (a₁ + a₂ ≡ b₁ + b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p]) :=
+λ ⟨m, hm⟩, (equiv.add_left m).symm.exists_congr_left.trans $
+  by simpa [add_sub_add_comm, hm, add_smul]
+
+@[simp] protected lemma add_iff_right :
+  a₂ ≡ b₂ [PMOD p] → (a₁ + a₂ ≡ b₁ + b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p]) :=
+λ ⟨m, hm⟩, (equiv.add_right m).symm.exists_congr_left.trans $
+  by simpa [add_sub_add_comm, hm, add_smul]
+
+@[simp] protected lemma sub_iff_left :
+  a₁ ≡ b₁ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₂ ≡ b₂ [PMOD p]) :=
+λ ⟨m, hm⟩, (equiv.sub_left m).symm.exists_congr_left.trans $
+  by simpa [sub_sub_sub_comm, hm, sub_smul]
+
+@[simp] protected lemma sub_iff_right :
+  a₂ ≡ b₂ [PMOD p] → (a₁ - a₂ ≡ b₁ - b₂ [PMOD p] ↔ a₁ ≡ b₁ [PMOD p]) :=
+λ ⟨m, hm⟩, (equiv.sub_right m).symm.exists_congr_left.trans $
+  by simpa [sub_sub_sub_comm, hm, sub_smul]
+
+alias modeq.add_iff_left ↔ add_left_cancel add
+alias modeq.add_iff_right ↔ add_right_cancel _
+alias modeq.sub_iff_left ↔ sub_left_cancel sub
+alias modeq.sub_iff_right ↔ sub_right_cancel _
+
+attribute [protected] add_left_cancel add_right_cancel add sub_left_cancel sub_right_cancel sub
+
+protected lemma add_left (c : α) (h : a ≡ b [PMOD p]) : c + a ≡ c + b [PMOD p] := modeq_rfl.add h
+protected lemma sub_left (c : α) (h : a ≡ b [PMOD p]) : c - a ≡ c - b [PMOD p] := modeq_rfl.sub h
+protected lemma add_right (c : α) (h : a ≡ b [PMOD p]) : a + c ≡ b + c [PMOD p] := h.add modeq_rfl
+protected lemma sub_right (c : α) (h : a ≡ b [PMOD p]) : a - c ≡ b - c [PMOD p] := h.sub modeq_rfl
+
+protected lemma add_left_cancel' (c : α) : c + a ≡ c + b [PMOD p] → a ≡ b [PMOD p] :=
+modeq_rfl.add_left_cancel
+
+protected lemma add_right_cancel' (c : α) : a + c ≡ b + c [PMOD p] → a ≡ b [PMOD p] :=
+modeq_rfl.add_right_cancel
+
+protected lemma sub_left_cancel' (c : α) : c - a ≡ c - b [PMOD p] → a ≡ b [PMOD p] :=
+modeq_rfl.sub_left_cancel
+
+protected lemma sub_right_cancel' (c : α) : a - c ≡ b - c [PMOD p] → a ≡ b [PMOD p] :=
+modeq_rfl.sub_right_cancel
+
+end modeq
+
+lemma modeq_sub_iff_add_modeq' : a ≡ b - c [PMOD p] ↔ c + a ≡ b [PMOD p] := by simp [modeq, sub_sub]
+lemma modeq_sub_iff_add_modeq : a ≡ b - c [PMOD p] ↔ a + c ≡ b [PMOD p] :=
+modeq_sub_iff_add_modeq'.trans $ by rw add_comm
+lemma sub_modeq_iff_modeq_add' : a - b ≡ c [PMOD p] ↔ a ≡ b + c [PMOD p] :=
+modeq_comm.trans $ modeq_sub_iff_add_modeq'.trans modeq_comm
+lemma sub_modeq_iff_modeq_add : a - b ≡ c [PMOD p] ↔ a ≡ c + b [PMOD p] :=
+modeq_comm.trans $ modeq_sub_iff_add_modeq.trans modeq_comm
+
+@[simp] lemma sub_modeq_zero : a - b ≡ 0 [PMOD p] ↔ a ≡ b [PMOD p] :=
+by simp [sub_modeq_iff_modeq_add]
+
+@[simp] lemma add_modeq_left : a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p] :=
+by simp [←modeq_sub_iff_add_modeq']
+
+@[simp] lemma add_modeq_right : a + b ≡ b [PMOD p] ↔ a ≡ 0 [PMOD p] :=
+by simp [←modeq_sub_iff_add_modeq]
+
+lemma modeq_iff_eq_add_zsmul : a ≡ b [PMOD p] ↔ ∃ z : ℤ, b = a + z • p :=
+by simp_rw [modeq, sub_eq_iff_eq_add']
+
+lemma not_modeq_iff_ne_add_zsmul : ¬a ≡ b [PMOD p] ↔ ∀ z : ℤ, b ≠ a + z • p :=
+by rw [modeq_iff_eq_add_zsmul, not_exists]
+
+lemma modeq_iff_eq_mod_zmultiples : a ≡ b [PMOD p] ↔ (b : α ⧸ add_subgroup.zmultiples p) = a :=
+by simp_rw [modeq_iff_eq_add_zsmul, quotient_add_group.eq_iff_sub_mem,
+    add_subgroup.mem_zmultiples_iff, eq_sub_iff_add_eq', eq_comm]
+
+lemma not_modeq_iff_ne_mod_zmultiples :
+  ¬a ≡ b [PMOD p] ↔ (b : α ⧸ add_subgroup.zmultiples p) ≠ a :=
+modeq_iff_eq_mod_zmultiples.not
+
+end add_comm_group
+
+@[simp] lemma modeq_iff_int_modeq {a b z : ℤ} : a ≡ b [PMOD z] ↔ a ≡ b [ZMOD z] :=
+by simp [modeq, dvd_iff_exists_eq_mul_left, int.modeq_iff_dvd]
+
+section add_comm_group_with_one
+variables [add_comm_group_with_one α] [char_zero α]
+
+@[simp, norm_cast]
+lemma int_cast_modeq_int_cast {a b z : ℤ} : a ≡ b [PMOD (z : α)] ↔ a ≡ b [PMOD z] :=
+by simp_rw [modeq, ←int.cast_mul_eq_zsmul_cast]; norm_cast
+
+@[simp, norm_cast]
+lemma nat_cast_modeq_nat_cast {a b n : ℕ} : a ≡ b [PMOD (n : α)] ↔ a ≡ b [MOD n] :=
+by simp_rw [←int.coe_nat_modeq_iff, ←modeq_iff_int_modeq, ←@int_cast_modeq_int_cast α,
+  int.cast_coe_nat]
+
+alias int_cast_modeq_int_cast ↔ modeq.of_int_cast modeq.int_cast
+alias nat_cast_modeq_nat_cast ↔ _root_.nat.modeq.of_nat_cast modeq.nat_cast
+
+end add_comm_group_with_one
+end add_comm_group
diff --git a/src/algebra/order/to_interval_mod.lean b/src/algebra/order/to_interval_mod.lean
diff --git a/src/topology/instances/add_circle.lean b/src/topology/instances/add_circle.lean
