Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2018 Chris Hughes. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Hughes
! This file was ported from Lean 3 source module data.int.modeq
! leanprover-community/mathlib commit 47a1a73351de8dd6c8d3d32b569c8e434b03ca47
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Std.Data.Int.DivMod
import Mathlib.Data.Nat.ModEq
import Mathlib.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 `n.ModEq a b`,
which is defined to be `a % n = b % n` for integers `a b n`.
## Tags
modeq, congruence, mod, MOD, modulo, integers
-/
namespace Int
/-- `a ≡ b [ZMOD n]` when `a % n = b % n`. -/
def ModEq : (n a b : ℤ ) → ?m.9 n a b ModEq ( n a b : ℤ ) :=
a % n = b % n
#align int.modeq Int.ModEq
@[inherit_doc]
notation :50 a " ≡ " b " [ZMOD " n "]" => ModEq n a b
variable { m n a b c d : ℤ }
-- Porting note: This instance should be derivable automatically
instance : Decidable ( ModEq n a b ) := decEq ( a % n ) ( b % n )
namespace ModEq
@[refl]
protected theorem refl ( a : ℤ ) : a ≡ a [ZMOD n ] :=
@ rfl : ∀ {α : Sort ?u.8988} {a : α }, a = a _ _
#align int.modeq.refl Int.ModEq.refl : ∀ {n : ℤ } (a : ℤ ), a ≡ a [ZMOD n ]
protected theorem rfl : a ≡ a [ZMOD n ] :=
ModEq.refl : ∀ {n : ℤ } (a : ℤ ), a ≡ a [ZMOD n ] _
#align int.modeq.rfl Int.ModEq.rfl : ∀ {n a : ℤ }, a ≡ a [ZMOD n ]
instance : IsRefl _ ( ModEq n ) :=
⟨ ModEq.refl : ∀ {n : ℤ } (a : ℤ ), a ≡ a [ZMOD n ] ⟩
@[symm]
protected theorem symm : a ≡ b [ZMOD n ] → b ≡ a [ZMOD n ] :=
Eq.symm : ∀ {α : Sort ?u.9094} {a b : α }, a = b b = a
#align int.modeq.symm Int.ModEq.symm
@[trans]
protected theorem trans : a ≡ b [ZMOD n ] → b ≡ c [ZMOD n ] → a ≡ c [ZMOD n ] :=
Eq.trans : ∀ {α : Sort ?u.9132} {a b c : α }, a = b b = c a = c
#align int.modeq.trans Int.ModEq.trans
instance : IsTrans ℤ ( ModEq n ) where
trans := @ Int.ModEq.trans n
protected theorem eq : a ≡ b [ZMOD n ] → a % n = b % n := id : ∀ {α : Sort ?u.9280}, α → α
#align int.modeq.eq Int.ModEq.eq : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] a % n = b % n
end ModEq
theorem modEq_comm : a ≡ b [ZMOD n ] ↔ b ≡ a [ZMOD n ] := ⟨ ModEq.symm , ModEq.symm ⟩
#align int.modeq_comm Int.modEq_comm
theorem coe_nat_modEq_iff { a b n : ℕ } : a ≡ b [ZMOD n ] ↔ a ≡ b [MOD n ] := by
m, n✝, a✝, b✝, c, d : ℤ a, b, n : ℕ unfold ModEq Nat.ModEq m, n✝, a✝, b✝, c, d : ℤ a, b, n : ℕ ; m, n✝, a✝, b✝, c, d : ℤ a, b, n : ℕ m, n✝, a✝, b✝, c, d : ℤ a, b, n : ℕ rw [ m, n✝, a✝, b✝, c, d : ℤ a, b, n : ℕ ← Int.ofNat_inj : ∀ {m n : ℕ }, ↑m = ↑n ↔ m = n m, n✝, a✝, b✝, c, d : ℤ a, b, n : ℕ ↑a % ↑n = ↑b % ↑n ↔ ↑(a % n = ↑(b % n ] m, n✝, a✝, b✝, c, d : ℤ a, b, n : ℕ ↑a % ↑n = ↑b % ↑n ↔ ↑(a % n = ↑(b % n ; m, n✝, a✝, b✝, c, d : ℤ a, b, n : ℕ ↑a % ↑n = ↑b % ↑n ↔ ↑(a % n = ↑(b % n m, n✝, a✝, b✝, c, d : ℤ a, b, n : ℕ simp [ coe_nat_mod : ∀ (m n : ℕ ), ↑(m % n = ↑m % ↑n ]
#align int.coe_nat_modeq_iff Int.coe_nat_modEq_iff
theorem modEq_zero_iff_dvd : a ≡ 0 [ZMOD n ] ↔ n ∣ a := by
rw [ ModEq , zero_emod : ∀ (b : ℤ ), 0 % b = 0 , dvd_iff_emod_eq_zero : ∀ (a b : ℤ ), a ∣ b ↔ b % a = 0 ]
#align int.modeq_zero_iff_dvd Int.modEq_zero_iff_dvd : ∀ {n a : ℤ }, a ≡ 0 [ZMOD n ] ↔ n ∣ a
theorem _root_.Dvd.dvd.modEq_zero_int : n ∣ a a ≡ 0 [ZMOD n ] _root_.Dvd.dvd.modEq_zero_int ( h : n ∣ a ) : a ≡ 0 [ZMOD n ] :=
modEq_zero_iff_dvd : ∀ {n a : ℤ }, a ≡ 0 [ZMOD n ] ↔ n ∣ a . 2 : ∀ {a b : Prop }, (a ↔ b b → a h
#align has_dvd.dvd.modeq_zero_int Dvd.dvd.modEq_zero_int : ∀ {n a : ℤ }, n ∣ a a ≡ 0 [ZMOD n ]
theorem _root_.Dvd.dvd.zero_modEq_int : n ∣ a 0 ≡ a [ZMOD n ] _root_.Dvd.dvd.zero_modEq_int ( h : n ∣ a ) : 0 ≡ a [ZMOD n ] :=
h . modEq_zero_int : ∀ {n a : ℤ }, n ∣ a a ≡ 0 [ZMOD n ] . symm
#align has_dvd.dvd.zero_modeq_int Dvd.dvd.zero_modEq_int : ∀ {n a : ℤ }, n ∣ a 0 ≡ a [ZMOD n ]
theorem modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a modEq_iff_dvd : a ≡ b [ZMOD n ] ↔ n ∣ b - a := by
rw [ ModEq , eq_comm : ∀ {α : Sort ?u.9963} {a b : α }, a = b ↔ b = a ]
simp [ emod_eq_emod_iff_emod_sub_eq_zero : ∀ {m n k : ℤ }, m % n = k % n ↔ (m - k % n = 0 , dvd_iff_emod_eq_zero : ∀ (a b : ℤ ), a ∣ b ↔ b % a = 0 ]
#align int.modeq_iff_dvd Int.modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a
theorem modEq_iff_add_fac : ∀ {a b n : ℤ }, a ≡ b [ZMOD n ] ↔ ∃ t , b = a + n * t modEq_iff_add_fac { a b n : ℤ } : a ≡ b [ZMOD n ] ↔ ∃ t , b = a + n * t := by
m, n✝, a✝, b✝, c, d, a, b, n : ℤ rw [ m, n✝, a✝, b✝, c, d, a, b, n : ℤ modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a m, n✝, a✝, b✝, c, d, a, b, n : ℤ n ∣ b - a ↔ ∃ t , b = a + n * t ] m, n✝, a✝, b✝, c, d, a, b, n : ℤ n ∣ b - a ↔ ∃ t , b = a + n * t
m, n✝, a✝, b✝, c, d, a, b, n : ℤ exact exists_congr : ∀ {α : Sort ?u.10422} {p q : α → Prop (∀ (a : α ), p a ↔ q a ) → ((∃ a , p a ) ↔ ∃ a , q a ) fun t => sub_eq_iff_eq_add'
#align int.modeq_iff_add_fac Int.modEq_iff_add_fac : ∀ {a b n : ℤ }, a ≡ b [ZMOD n ] ↔ ∃ t , b = a + n * t
alias modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a ↔ ModEq.dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] n ∣ b - a modEq_of_dvd : ∀ {n a b : ℤ }, n ∣ b - a a ≡ b [ZMOD n ]
#align int.modeq.dvd Int.ModEq.dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] n ∣ b - a
#align int.modeq_of_dvd Int.modEq_of_dvd : ∀ {n a b : ℤ }, n ∣ b - a a ≡ b [ZMOD n ]
theorem mod_modEq ( a n ) : a % n ≡ a [ZMOD n ] :=
emod_emod : ∀ (a b : ℤ ), a % b % b = a % b _ _
#align int.mod_modeq Int.mod_modEq : ∀ (a n : ℤ ), a % n ≡ a [ZMOD n ]
@[ simp ]
theorem neg_modEq_neg : - a ≡ - b [ZMOD n ] ↔ a ≡ b [ZMOD n ] := by
--porting note: Restore old proof once #3309 is through
simp [- sub_neg_eq_add , neg_sub_neg , modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a , dvd_sub_comm ]
#align int.neg_modeq_neg Int.neg_modEq_neg
@[ simp ]
theorem modEq_neg : a ≡ b [ZMOD - n ] ↔ a ≡ b [ZMOD n ] := by simp [ modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a ]
#align int.modeq_neg Int.modEq_neg
namespace ModEq
protected theorem of_dvd ( d : m ∣ n ) ( h : a ≡ b [ZMOD n ]) : a ≡ b [ZMOD m ] :=
modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a . 2 : ∀ {a b : Prop }, (a ↔ b b → a <| d . trans : ∀ {α : Type ?u.14056} [inst : Semigroup α a b c : α }, a ∣ b b ∣ c a ∣ c h . dvd
#align int.modeq.of_dvd Int.ModEq.of_dvd
protected theorem mul_left' ( h : a ≡ b [ZMOD n ]) : c * a ≡ c * b [ZMOD c * n ] := by
obtain hc hc | rfl | hc : c < 0 ∨ c = 0 ∨ 0 < c rfl hc | rfl | hc : c < 0 ∨ c = 0 ∨ 0 < c hc := lt_trichotomy c 0 m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl inr.inl m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : 0 < c inr.inr
· m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl inr.inl m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : 0 < c inr.inr rw [ m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl ← neg_modEq_neg , m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl ← modEq_neg , m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl ← neg_mul , m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl ← neg_mul , m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl ← neg_mul m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl ] m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl
m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : c < 0 inl simp only [ ModEq , mul_emod_mul_of_pos : ∀ {a : ℤ } (b c : ℤ ), 0 < a a * b % (a * c = a * (b % c _ _ ( neg_pos . 2 : ∀ {a b : Prop }, (a ↔ b b → a hc ), h . eq ]
· inr.inl m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : 0 < c inr.inr simp
· m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : 0 < c inr.inr m, n, a, b, c, d : ℤ h : a ≡ b [ZMOD n ] hc : 0 < c inr.inr simp only [ ModEq , mul_emod_mul_of_pos : ∀ {a : ℤ } (b c : ℤ ), 0 < a a * b % (a * c = a * (b % c _ _ hc , h . eq ]
#align int.modeq.mul_left' Int.ModEq.mul_left'
protected theorem mul_right' ( h : a ≡ b [ZMOD n ]) : a * c ≡ b * c [ZMOD n * c ] := by
rw [ mul_comm a , mul_comm b , mul_comm n ] ; exact h . mul_left'
#align int.modeq.mul_right' Int.ModEq.mul_right'
protected theorem add ( h₁ : a ≡ b [ZMOD n ]) ( h₂ : c ≡ d [ZMOD n ]) : a + c ≡ b + d [ZMOD n ] :=
modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a . 2 : ∀ {a b : Prop }, (a ↔ b b → a <| by
convert dvd_add h₁ . dvd h₂ . dvd using 1
ring
#align int.modeq.add Int.ModEq.add
protected theorem add_left ( c : ℤ ) ( h : a ≡ b [ZMOD n ]) : c + a ≡ c + b [ZMOD n ] :=
ModEq.rfl . add h
#align int.modeq.add_left Int.ModEq.add_left
protected theorem add_right ( c : ℤ ) ( h : a ≡ b [ZMOD n ]) : a + c ≡ b + c [ZMOD n ] :=
h . add ModEq.rfl
#align int.modeq.add_right Int.ModEq.add_right
protected theorem add_left_cancel ( h₁ : a ≡ b [ZMOD n ]) ( h₂ : a + c ≡ b + d [ZMOD n ]) :
c ≡ d [ZMOD n ] :=
have : d - c = b + d - ( a + c ) - ( b - a ) := by ring
modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a . 2 : ∀ {a b : Prop }, (a ↔ b b → a <| by
rw [ this : d - c = b + d - (a + c - (b - a this ]
exact dvd_sub h₂ . dvd h₁ . dvd
#align int.modeq.add_left_cancel Int.ModEq.add_left_cancel
protected theorem add_left_cancel' ( c : ℤ ) ( h : c + a ≡ c + b [ZMOD n ]) : a ≡ b [ZMOD n ] :=
ModEq.rfl . add_left_cancel h
#align int.modeq.add_left_cancel' Int.ModEq.add_left_cancel' : ∀ {n a b : ℤ } (c : ℤ ), c + a ≡ c + b [ZMOD n ] a ≡ b [ZMOD n ]
protected theorem add_right_cancel ( h₁ : c ≡ d [ZMOD n ]) ( h₂ : a + c ≡ b + d [ZMOD n ]) :
a ≡ b [ZMOD n ] := by
rw [ add_comm a , add_comm b ] at h₂
exact h₁ . add_left_cancel h₂
#align int.modeq.add_right_cancel Int.ModEq.add_right_cancel
protected theorem add_right_cancel' ( c : ℤ ) ( h : a + c ≡ b + c [ZMOD n ]) : a ≡ b [ZMOD n ] :=
ModEq.rfl . add_right_cancel h
#align int.modeq.add_right_cancel' Int.ModEq.add_right_cancel' : ∀ {n a b : ℤ } (c : ℤ ), a + c ≡ b + c [ZMOD n ] a ≡ b [ZMOD n ]
protected theorem neg ( h : a ≡ b [ZMOD n ]) : - a ≡ - b [ZMOD n ] :=
h . add_left_cancel ( by simp_rw [ ← sub_eq_add_neg , sub_self : ∀ {G : Type ?u.18097} [inst : AddGroup G a : G ), a - a = 0 ] ; rfl )
#align int.modeq.neg Int.ModEq.neg
protected theorem sub ( h₁ : a ≡ b [ZMOD n ]) ( h₂ : c ≡ d [ZMOD n ]) : a - c ≡ b - d [ZMOD n ] := by
rw [ sub_eq_add_neg , sub_eq_add_neg ]
exact h₁ . add h₂ . neg
#align int.modeq.sub Int.ModEq.sub
protected theorem sub_left ( c : ℤ ) ( h : a ≡ b [ZMOD n ]) : c - a ≡ c - b [ZMOD n ] :=
ModEq.rfl . sub h
#align int.modeq.sub_left Int.ModEq.sub_left
protected theorem sub_right ( c : ℤ ) ( h : a ≡ b [ZMOD n ]) : a - c ≡ b - c [ZMOD n ] :=
h . sub ModEq.rfl
#align int.modeq.sub_right Int.ModEq.sub_right
protected theorem mul_left ( c : ℤ ) ( h : a ≡ b [ZMOD n ]) : c * a ≡ c * b [ZMOD n ] :=
h . mul_left' . of_dvd <| dvd_mul_left _ _
#align int.modeq.mul_left Int.ModEq.mul_left
protected theorem mul_right ( c : ℤ ) ( h : a ≡ b [ZMOD n ]) : a * c ≡ b * c [ZMOD n ] :=
h . mul_right' . of_dvd <| dvd_mul_right : ∀ {α : Type ?u.18906} [inst : Semigroup α a b : α ), a ∣ a * b _ _
#align int.modeq.mul_right Int.ModEq.mul_right
protected theorem mul ( h₁ : a ≡ b [ZMOD n ]) ( h₂ : c ≡ d [ZMOD n ]) : a * c ≡ b * d [ZMOD n ] :=
( h₂ . mul_left _ ). trans ( h₁ . mul_right _ )
#align int.modeq.mul Int.ModEq.mul
protected theorem pow ( m : ℕ ) ( h : a ≡ b [ZMOD n ]) : a ^ m ≡ b ^ m [ZMOD n ] := by
induction' m with d hd ; · rfl
rw [ pow_succ : ∀ {M : Type ?u.19405} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a * a ^ n , pow_succ : ∀ {M : Type ?u.19488} [inst : Monoid M a : M ) (n : ℕ ), a ^ (n + 1 = a * a ^ n ]
exact h . mul hd
#align int.modeq.pow Int.ModEq.pow
lemma of_mul_left ( m : ℤ ) ( h : a ≡ b [ZMOD m * n ]) : a ≡ b [ZMOD n ] := by
rw [ modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a m✝, n, a, b, c, d : ℤ of_mul_left : ∀ (m : ℤ ), a ≡ b [ZMOD m * n ] n ∣ b - a m : ℤ h : m * n ∣ b - a ] m✝, n, a, b, c, d : ℤ of_mul_left : ∀ (m : ℤ ), a ≡ b [ZMOD m * n ] n ∣ b - a m : ℤ h : m * n ∣ b - a at * m✝, n, a, b, c, d : ℤ of_mul_left : ∀ (m : ℤ ), a ≡ b [ZMOD m * n ] n ∣ b - a m : ℤ h : m * n ∣ b - a ; m✝, n, a, b, c, d : ℤ of_mul_left : ∀ (m : ℤ ), a ≡ b [ZMOD m * n ] n ∣ b - a m : ℤ h : m * n ∣ b - a exact ( dvd_mul_left n m ). trans : ∀ {α : Type ?u.19794} [inst : Semigroup α a b c : α }, a ∣ b b ∣ c a ∣ c trans h
#align int.modeq.of_mul_left Int.ModEq.of_mul_left
lemma of_mul_right ( m : ℤ ) : a ≡ b [ZMOD n * m ] → a ≡ b [ZMOD n ] :=
mul_comm m n ▸ of_mul_left _
#align int.modeq.of_mul_right Int.ModEq.of_mul_right
/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`. -/
theorem cancel_right_div_gcd ( hm : 0 < m ) ( h : a * c ≡ b * c [ZMOD m ]) :
a ≡ b [ZMOD m / gcd m c ] := by
letI d := gcd m c
have hmd := gcd_dvd_left : ∀ (i j : ℤ ), ↑(gcd i j ∣ i m c
have hcd := gcd_dvd_right : ∀ (i j : ℤ ), ↑(gcd i j ∣ j m c
rw [ modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c ] m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c at h ⊢ m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c
-- porting note: removed `show` due to leanprover-community/mathlib4#3305
refine Int.dvd_of_dvd_mul_right_of_gcd_one : ∀ {a b c : ℤ }, a ∣ b * c gcd a b = 1 a ∣ c ( ?_ : m / ↑d ∣ c / ↑d * (b - a : m / d ∣ c / d * ( b - a )) ?_ : gcd ?m.20300 ?m.20301 = 1 m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_1 m / ↑d ∣ c / ↑d * (b - a m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_2
· m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_1 m / ↑d ∣ c / ↑d * (b - a m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_1 m / ↑d ∣ c / ↑d * (b - a m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_2 rw [ m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_1 m / ↑d ∣ c / ↑d * (b - a mul_comm , m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_1 m / ↑d ∣ (b - a * (c / ↑d m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_1 m / ↑d ∣ c / ↑d * (b - a ← Int.mul_ediv_assoc : ∀ (a : ℤ ) {b c : ℤ }, c ∣ b a * b / c = a * (b / c ( b - a ) hcd , m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_1 m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_1 m / ↑d ∣ c / ↑d * (b - a sub_mul m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_1 ] m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_1
m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_1 m / ↑d ∣ c / ↑d * (b - a exact Int.ediv_dvd_ediv : ∀ {a b c : ℤ }, a ∣ b b ∣ c b / a ∣ c / a hmd h
· m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_2 m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_2 rw [ m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_2 gcd_div hmd hcd , m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_2 m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_2 natAbs_ofNat , m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_2 m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_2 Nat.div_self : ∀ {n : ℕ }, 0 < n n / n = 1 ( gcd_pos_of_ne_zero_left : ∀ {i : ℤ } (j : ℤ ), i ≠ 0 0 < gcd i j c hm . ne' : ∀ {α : Type ?u.20762} [inst : Preorder α x y : α }, x < y y ≠ x ) m, n, a, b, c, d✝ : ℤ hm : 0 < m h : m ∣ b * c - a * c d := gcd m c : ℕ hmd : ↑(gcd m c ∣ m hcd : ↑(gcd m c ∣ c refine_2 ]
#align int.modeq.cancel_right_div_gcd Int.ModEq.cancel_right_div_gcd
/-- To cancel a common factor `c` from a `ModEq` we must divide the modulus `m` by `gcd m c`. -/
theorem cancel_left_div_gcd ( hm : 0 < m ) ( h : c * a ≡ c * b [ZMOD m ]) : a ≡ b [ZMOD m / gcd m c ] :=
cancel_right_div_gcd hm <| by simpa [ mul_comm ] using h
#align int.modeq.cancel_left_div_gcd Int.ModEq.cancel_left_div_gcd
theorem of_div ( h : a / c ≡ b / c [ZMOD m / c ]) ( ha : c ∣ a ) ( ha : c ∣ b ) ( ha : c ∣ m ) :
a ≡ b [ZMOD m ] := by m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m convert h . mul_left' m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m h.e'_1 m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m h.e'_2 m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m h.e'_3 m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m <;> m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m h.e'_1 m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m h.e'_2 m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m h.e'_3 m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m rwa [ m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m h.e'_2 Int.mul_ediv_cancel' : ∀ {a b : ℤ }, a ∣ b a * (b / a = b m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m h.e'_3 m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m h.e'_3 ] m, n, a, b, c, d : ℤ h : a / c ≡ b / c [ZMOD m / c ] ha✝¹ : c ∣ a ha✝ : c ∣ b ha : c ∣ m h.e'_1
#align int.modeq.of_div Int.ModEq.of_div
end ModEq
theorem modEq_one : a ≡ b [ZMOD 1 ] :=
modEq_of_dvd : ∀ {n a b : ℤ }, n ∣ b - a a ≡ b [ZMOD n ] ( one_dvd : ∀ {α : Type ?u.23668} [inst : Monoid α a : α ), 1 ∣ a _ )
#align int.modeq_one Int.modEq_one : ∀ {a b : ℤ }, a ≡ b [ZMOD 1 ]
theorem modEq_sub ( a b : ℤ ) : a ≡ b [ZMOD a - b ] :=
( modEq_of_dvd : ∀ {n a b : ℤ }, n ∣ b - a a ≡ b [ZMOD n ] dvd_rfl : ∀ {α : Type ?u.23792} [inst : Monoid α a : α }, a ∣ a ). symm
#align int.modeq_sub Int.modEq_sub : ∀ (a b : ℤ ), a ≡ b [ZMOD a - b ]
@[ simp ]
theorem modEq_zero_iff : ∀ {a b : ℤ }, a ≡ b [ZMOD 0 ] ↔ a = b modEq_zero_iff : a ≡ b [ZMOD 0 ] ↔ a = b := by rw [ ModEq , emod_zero : ∀ (a : ℤ ), a % 0 = a , emod_zero : ∀ (a : ℤ ), a % 0 = a ]
#align int.modeq_zero_iff Int.modEq_zero_iff : ∀ {a b : ℤ }, a ≡ b [ZMOD 0 ] ↔ a = b
@[ simp ]
theorem add_modEq_left : ∀ {n a : ℤ }, n + a ≡ a [ZMOD n ] add_modEq_left : n + a ≡ a [ZMOD n ] := ModEq.symm <| modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a . 2 : ∀ {a b : Prop }, (a ↔ b b → a <| by simp
#align int.add_modeq_left Int.add_modEq_left : ∀ {n a : ℤ }, n + a ≡ a [ZMOD n ]
@[ simp ]
theorem add_modEq_right : a + n ≡ a [ZMOD n ] := ModEq.symm <| modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a . 2 : ∀ {a b : Prop }, (a ↔ b b → a <| by simp
#align int.add_modeq_right Int.add_modEq_right : ∀ {n a : ℤ }, a + n ≡ a [ZMOD n ]
theorem modEq_and_modEq_iff_modEq_mul { a b m n : ℤ } ( hmn : m . natAbs . coprime n . natAbs ) :
a ≡ b [ZMOD m ] ∧ a ≡ b [ZMOD n ] ↔ a ≡ b [ZMOD m * n ] :=
⟨ fun h => by
rw [ modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a , modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a ] at h
rw [ modEq_iff_dvd : ∀ {n a b : ℤ }, a ≡ b [ZMOD n ] ↔ n ∣ b - a , ← natAbs_dvd , ← dvd_natAbs , coe_nat_dvd : ∀ {m n : ℕ }, ↑m ∣ ↑n ↔ m ∣ n , natAbs_mul ]
refine' hmn . mul_dvd_of_dvd_of_dvd : ∀ {m n a : ℕ }, Nat.coprime m n m ∣ a n ∣ a m * n ∣ a _ _ <;> rw [ ← coe_nat_dvd : ∀ {m n : ℕ }, ↑m ∣ ↑n ↔ m ∣ n , natAbs_dvd , dvd_natAbs