Mathlib.Data.Int.ModEq

Int.ModEq definition

(n a b : ℤ)

Full source

/-- `a ≡ b [ZMOD n]` when `a % n = b % n`. -/
def ModEq (n a b : ℤ) :=
  a % n = b % n

Congruence modulo an integer

Informal description

For integers $a$, $b$, and $n$, the relation $a \equiv b \pmod{n}$ holds when $a$ modulo $n$ is equal to $b$ modulo $n$, i.e., $a \% n = b \% n$.

Int.term_≡_[ZMOD_] definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc]
notation:50 a " ≡ " b " [ZMOD " n "]" => ModEq n a b

Congruence modulo an integer

Informal description

The notation `a ≡ b [ZMOD n]` denotes the congruence relation modulo an integer `n`, meaning that `a` and `b` leave the same remainder when divided by `n`. Formally, this is defined as `a % n = b % n`.

Int.instDecidableModEq instance

: Decidable (ModEq n a b)

Full source

instance : Decidable (ModEq n a b) := decEq (a % n) (b % n)

Decidability of Integer Congruence

Informal description

For any integers $n$, $a$, and $b$, the congruence relation $a \equiv b \pmod{n}$ is decidable.

Int.ModEq.refl theorem

(a : ℤ) : a ≡ a [ZMOD n]

Full source

@[refl, simp]
protected theorem refl (a : ℤ) : a ≡ a [ZMOD n] :=
  @rfl _ _

Reflexivity of Congruence Modulo $n$

Informal description

For any integer $a$, the congruence relation $a \equiv a \pmod{n}$ holds for any integer modulus $n$.

Int.ModEq.rfl theorem

: a ≡ a [ZMOD n]

Full source

protected theorem rfl : a ≡ a [ZMOD n] :=
  ModEq.refl _

Reflexivity of Congruence Modulo $n$

Informal description

For any integer $a$, the congruence relation $a \equiv a \pmod{n}$ holds for any integer modulus $n$.

Int.ModEq.instIsRefl instance

: IsRefl _ (ModEq n)

Full source

instance : IsRefl _ (ModEq n) :=
  ⟨ModEq.refl⟩

Reflexivity of Integer Congruence Modulo $n$

Informal description

For any integer modulus $n$, the congruence relation $\equiv \pmod{n}$ is reflexive on the integers. That is, for any integer $a$, we have $a \equiv a \pmod{n}$.

Int.ModEq.symm theorem

: a ≡ b [ZMOD n] → b ≡ a [ZMOD n]

Full source

@[symm]
protected theorem symm : a ≡ b [ZMOD n] → b ≡ a [ZMOD n] :=
  Eq.symm

Symmetry of Congruence Modulo $n$

Informal description

For any integers $a$, $b$, and $n$, if $a \equiv b \pmod{n}$, then $b \equiv a \pmod{n}$.

Int.ModEq.trans theorem

: a ≡ b [ZMOD n] → b ≡ c [ZMOD n] → a ≡ c [ZMOD n]

Full source

@[trans]
protected theorem trans : a ≡ b [ZMOD n] → b ≡ c [ZMOD n] → a ≡ c [ZMOD n] :=
  Eq.trans

Transitivity of Congruence Modulo an Integer

Informal description

For integers $a$, $b$, $c$, and $n$, if $a \equiv b \pmod{n}$ and $b \equiv c \pmod{n}$, then $a \equiv c \pmod{n}$.

Int.ModEq.instIsTrans instance

: IsTrans ℤ (ModEq n)

Full source

instance : IsTrans ℤ (ModEq n) where
  trans := @Int.ModEq.trans n

Transitivity of Congruence Modulo $n$

Informal description

The relation $a \equiv b \pmod{n}$ on the integers is transitive.

Int.ModEq.eq theorem

: a ≡ b [ZMOD n] → a % n = b % n

Full source

protected theorem eq : a ≡ b [ZMOD n] → a % n = b % n := id

Congruence Implies Equal Remainders

Informal description

For integers $a$, $b$, and $n$, if $a \equiv b \pmod{n}$, then the remainders of $a$ and $b$ when divided by $n$ are equal, i.e., $a \% n = b \% n$.

Int.modEq_comm theorem

: a ≡ b [ZMOD n] ↔ b ≡ a [ZMOD n]

Full source

theorem modEq_comm : a ≡ b [ZMOD n]a ≡ b [ZMOD n] ↔ b ≡ a [ZMOD n] := ⟨ModEq.symm, ModEq.symm⟩

Commutativity of Congruence Modulo $n$

Informal description

For any integers $a$, $b$, and $n$, the congruence $a \equiv b \pmod{n}$ holds if and only if $b \equiv a \pmod{n}$.

Int.natCast_modEq_iff theorem

{a b n : ℕ} : a ≡ b [ZMOD n] ↔ a ≡ b [MOD n]

Full source

theorem natCast_modEq_iff {a b n : ℕ} : a ≡ b [ZMOD n]a ≡ b [ZMOD n] ↔ a ≡ b [MOD n] := by
  unfold ModEq Nat.ModEq; rw [← Int.ofNat_inj]; simp [natCast_mod]

Equivalence of Integer and Natural Number Congruence for Natural Numbers

Informal description

For natural numbers $a$, $b$, and $n$, the congruence $a \equiv b \pmod{n}$ holds in the integers if and only if it holds in the natural numbers.

Int.modEq_zero_iff_dvd theorem

: a ≡ 0 [ZMOD n] ↔ n ∣ a

Full source

theorem modEq_zero_iff_dvd : a ≡ 0 [ZMOD n]a ≡ 0 [ZMOD n] ↔ n ∣ a := by
  rw [ModEq, zero_emod, dvd_iff_emod_eq_zero]

Congruence to Zero Modulo $n$ is Equivalent to Divisibility by $n$

Informal description

For integers $a$ and $n$, the congruence $a \equiv 0 \pmod{n}$ holds if and only if $n$ divides $a$, i.e., $n \mid a$.

Dvd.dvd.modEq_zero_int theorem

(h : n ∣ a) : a ≡ 0 [ZMOD n]

Full source

theorem _root_.Dvd.dvd.modEq_zero_int (h : n ∣ a) : a ≡ 0 [ZMOD n] :=
  modEq_zero_iff_dvd.2 h

Divisibility Implies Congruence to Zero Modulo $n$

Informal description

For integers $a$ and $n$, if $n$ divides $a$ (i.e., $n \mid a$), then $a \equiv 0 \pmod{n}$.

Dvd.dvd.zero_modEq_int theorem

(h : n ∣ a) : 0 ≡ a [ZMOD n]

Full source

theorem _root_.Dvd.dvd.zero_modEq_int (h : n ∣ a) : 0 ≡ a [ZMOD n] :=
  h.modEq_zero_int.symm

Zero Congruent to $a$ Modulo $n$ when $n$ Divides $a$

Informal description

For integers $a$ and $n$, if $n$ divides $a$ (i.e., $n \mid a$), then $0 \equiv a \pmod{n}$.

Int.modEq_iff_dvd theorem

: a ≡ b [ZMOD n] ↔ n ∣ b - a

Full source

theorem modEq_iff_dvd : a ≡ b [ZMOD n]a ≡ b [ZMOD n] ↔ n ∣ b - a := by
  rw [ModEq, eq_comm]
  simp [emod_eq_emod_iff_emod_sub_eq_zero, dvd_iff_emod_eq_zero]

Characterization of Congruence Modulo $n$ via Divisibility

Informal description

For integers $a$, $b$, and $n$, the congruence $a \equiv b \pmod{n}$ holds if and only if $n$ divides the difference $b - a$.

Int.modEq_iff_add_fac theorem

{a b n : ℤ} : a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t

Full source

theorem modEq_iff_add_fac {a b n : ℤ} : a ≡ b [ZMOD n]a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t := by
  rw [modEq_iff_dvd]
  exact exists_congr fun t => sub_eq_iff_eq_add'

Congruence Modulo $n$ as Linear Combination

Informal description

For integers $a$, $b$, and $n$, the congruence $a \equiv b \pmod{n}$ holds if and only if there exists an integer $t$ such that $b = a + n \cdot t$.

Int.mod_modEq theorem

(a n) : a % n ≡ a [ZMOD n]

Full source

theorem mod_modEq (a n) : a % n ≡ a [ZMOD n] :=
  emod_emod _ _

Congruence of Remainder to Dividend Modulo $n$

Informal description

For any integers $a$ and $n$, the remainder of $a$ divided by $n$ is congruent to $a$ modulo $n$, i.e., $a \% n \equiv a \pmod{n}$.

Int.neg_modEq_neg theorem

: -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n]

Full source

@[simp]
theorem neg_modEq_neg : -a ≡ -b [ZMOD n]-a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n] := by
  simp only [modEq_iff_dvd, (by omega : -b - -a = -(b - a)), Int.dvd_neg]

Negation Preserves Congruence Modulo $n$

Informal description

For any integers $a$, $b$, and $n$, the congruence $-a \equiv -b \pmod{n}$ holds if and only if $a \equiv b \pmod{n}$.

Int.modEq_neg theorem

: a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n]

Full source

@[simp]
theorem modEq_neg : a ≡ b [ZMOD -n]a ≡ b [ZMOD -n] ↔ a ≡ b [ZMOD n] := by simp [modEq_iff_dvd]

Congruence Relation Invariance Under Sign Change: $a \equiv b \pmod{-n} \leftrightarrow a \equiv b \pmod{n}$

Informal description

For any integers $a$, $b$, and $n$, the congruence $a \equiv b \pmod{-n}$ holds if and only if $a \equiv b \pmod{n}$.

Int.ModEq.of_dvd theorem

(d : m ∣ n) (h : a ≡ b [ZMOD n]) : a ≡ b [ZMOD m]

Full source

protected theorem of_dvd (d : m ∣ n) (h : a ≡ b [ZMOD n]) : a ≡ b [ZMOD m] :=
  modEq_iff_dvd.2 <| d.trans h.dvd

Congruence Modulo Divisor Implies Congruence Modulo Factor: $m \mid n \land a \equiv b \pmod{n} \Rightarrow a \equiv b \pmod{m}$

Informal description

For integers $a$, $b$, $m$, and $n$, if $m$ divides $n$ and $a \equiv b \pmod{n}$, then $a \equiv b \pmod{m}$.

Int.ModEq.mul_left' theorem

(h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n]

Full source

protected theorem mul_left' (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD c * n] := by
  obtain hc | rfl | hc := lt_trichotomy c 0
  · rw [← neg_modEq_neg, ← modEq_neg, ← Int.neg_mul, ← Int.neg_mul, ← Int.neg_mul]
    simp only [ModEq, mul_emod_mul_of_pos _ _ (neg_pos.2 hc), h.eq]
  · simp only [Int.zero_mul, ModEq.rfl]
  · simp only [ModEq, mul_emod_mul_of_pos _ _ hc, h.eq]

Left Multiplication Preserves Congruence Modulo Scaled Divisor

Informal description

For any integers $a$, $b$, $c$, and $n$, if $a \equiv b \pmod{n}$, then $c \cdot a \equiv c \cdot b \pmod{c \cdot n}$.

Int.ModEq.mul_right' theorem

(h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n * c]

Full source

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'

Right Multiplication Preserves Congruence Modulo Scaled Divisor

Informal description

For any integers $a$, $b$, $c$, and $n$, if $a \equiv b \pmod{n}$, then $a \cdot c \equiv b \cdot c \pmod{n \cdot c}$.

Int.ModEq.add theorem

(h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a + c ≡ b + d [ZMOD n]

Full source

@[gcongr]
protected theorem add (h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a + c ≡ b + d [ZMOD n] :=
  modEq_iff_dvd.2 <| by convert Int.dvd_add h₁.dvd h₂.dvd using 1; omega

Addition Preserves Congruence Modulo $n$

Informal description

For integers $a, b, c, d, n$, if $a \equiv b \pmod{n}$ and $c \equiv d \pmod{n}$, then $a + c \equiv b + d \pmod{n}$.

Int.ModEq.add_left theorem

(c : ℤ) (h : a ≡ b [ZMOD n]) : c + a ≡ c + b [ZMOD n]

Full source

@[gcongr] protected theorem add_left (c : ℤ) (h : a ≡ b [ZMOD n]) : c + a ≡ c + b [ZMOD n] :=
  ModEq.rfl.add h

Left Addition Preserves Congruence Modulo $n$

Informal description

For any integers $a$, $b$, $c$, and $n$, if $a \equiv b \pmod{n}$, then $c + a \equiv c + b \pmod{n}$.

Int.ModEq.add_right theorem

(c : ℤ) (h : a ≡ b [ZMOD n]) : a + c ≡ b + c [ZMOD n]

Full source

@[gcongr] protected theorem add_right (c : ℤ) (h : a ≡ b [ZMOD n]) : a + c ≡ b + c [ZMOD n] :=
  h.add ModEq.rfl

Right Addition Preserves Congruence Modulo $n$

Informal description

For any integers $a$, $b$, $c$, and $n$, if $a \equiv b \pmod{n}$, then $a + c \equiv b + c \pmod{n}$.

Int.ModEq.add_left_cancel theorem

(h₁ : a ≡ b [ZMOD n]) (h₂ : a + c ≡ b + d [ZMOD n]) : c ≡ d [ZMOD n]

Full source

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 omega
  modEq_iff_dvd.2 <| by
    rw [this]
    exact Int.dvd_sub h₂.dvd h₁.dvd

Left Cancellation Property of Addition in Congruence Modulo $n$

Informal description

For integers $a, b, c, d, n$, if $a \equiv b \pmod{n}$ and $a + c \equiv b + d \pmod{n}$, then $c \equiv d \pmod{n}$.

Int.ModEq.add_left_cancel' theorem

(c : ℤ) (h : c + a ≡ c + b [ZMOD n]) : a ≡ b [ZMOD n]

Full source

protected theorem add_left_cancel' (c : ℤ) (h : c + a ≡ c + b [ZMOD n]) : a ≡ b [ZMOD n] :=
  ModEq.rfl.add_left_cancel h

Left Cancellation of Addition in Congruence Modulo $n$

Informal description

For any integers $a$, $b$, $c$, and $n$, if $c + a \equiv c + b \pmod{n}$, then $a \equiv b \pmod{n}$.

Int.ModEq.add_right_cancel theorem

(h₁ : c ≡ d [ZMOD n]) (h₂ : a + c ≡ b + d [ZMOD n]) : a ≡ b [ZMOD n]

Full source

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₂

Right Cancellation Property of Addition in Congruence Modulo $n$

Informal description

For integers $a, b, c, d, n$, if $c \equiv d \pmod{n}$ and $a + c \equiv b + d \pmod{n}$, then $a \equiv b \pmod{n}$.

Int.ModEq.add_right_cancel' theorem

(c : ℤ) (h : a + c ≡ b + c [ZMOD n]) : a ≡ b [ZMOD n]

Full source

protected theorem add_right_cancel' (c : ℤ) (h : a + c ≡ b + c [ZMOD n]) : a ≡ b [ZMOD n] :=
  ModEq.rfl.add_right_cancel h

Right Cancellation of Addition in Congruence Modulo $n$

Informal description

For any integers $a$, $b$, $c$, and $n$, if $a + c \equiv b + c \pmod{n}$, then $a \equiv b \pmod{n}$.

Int.ModEq.neg theorem

(h : a ≡ b [ZMOD n]) : -a ≡ -b [ZMOD n]

Full source

@[gcongr] 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]; rfl)

Negation Preserves Congruence Modulo $n$

Informal description

For integers $a$, $b$, and $n$, if $a \equiv b \pmod{n}$, then $-a \equiv -b \pmod{n}$.

Int.ModEq.sub theorem

(h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a - c ≡ b - d [ZMOD n]

Full source

@[gcongr]
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

Subtraction Preserves Congruence Modulo $n$

Informal description

For integers $a, b, c, d, n$, if $a \equiv b \pmod{n}$ and $c \equiv d \pmod{n}$, then $a - c \equiv b - d \pmod{n}$.

Int.ModEq.sub_left theorem

(c : ℤ) (h : a ≡ b [ZMOD n]) : c - a ≡ c - b [ZMOD n]

Full source

@[gcongr] protected theorem sub_left (c : ℤ) (h : a ≡ b [ZMOD n]) : c - a ≡ c - b [ZMOD n] :=
  ModEq.rfl.sub h

Left Subtraction Preserves Congruence Modulo $n$

Informal description

For any integers $a$, $b$, $c$, and $n$, if $a \equiv b \pmod{n}$, then $c - a \equiv c - b \pmod{n}$.

Int.ModEq.sub_right theorem

(c : ℤ) (h : a ≡ b [ZMOD n]) : a - c ≡ b - c [ZMOD n]

Full source

@[gcongr] protected theorem sub_right (c : ℤ) (h : a ≡ b [ZMOD n]) : a - c ≡ b - c [ZMOD n] :=
  h.sub ModEq.rfl

Right Subtraction Preserves Congruence Modulo $n$

Informal description

For any integers $a$, $b$, $c$, and $n$, if $a \equiv b \pmod{n}$, then $a - c \equiv b - c \pmod{n}$.

Int.ModEq.mul_left theorem

(c : ℤ) (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD n]

Full source

@[gcongr] protected theorem mul_left (c : ℤ) (h : a ≡ b [ZMOD n]) : c * a ≡ c * b [ZMOD n] :=
  h.mul_left'.of_dvd <| dvd_mul_left _ _

Left Multiplication Preserves Congruence Modulo $n$

Informal description

For any integers $a$, $b$, $c$, and $n$, if $a \equiv b \pmod{n}$, then $c \cdot a \equiv c \cdot b \pmod{n}$.

Int.ModEq.mul_right theorem

(c : ℤ) (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n]

Full source

@[gcongr] protected theorem mul_right (c : ℤ) (h : a ≡ b [ZMOD n]) : a * c ≡ b * c [ZMOD n] :=
  h.mul_right'.of_dvd <| dvd_mul_right _ _

Right Multiplication Preserves Congruence Modulo $n$

Informal description

For any integers $a$, $b$, $c$, and $n$, if $a \equiv b \pmod{n}$, then $a \cdot c \equiv b \cdot c \pmod{n}$.

Int.ModEq.mul theorem

(h₁ : a ≡ b [ZMOD n]) (h₂ : c ≡ d [ZMOD n]) : a * c ≡ b * d [ZMOD n]

Full source

@[gcongr]
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 _)

Multiplication Preserves Congruence Modulo $n$

Informal description

For integers $a, b, c, d, n$, if $a \equiv b \pmod{n}$ and $c \equiv d \pmod{n}$, then $a \cdot c \equiv b \cdot d \pmod{n}$.

Int.ModEq.pow theorem

(m : ℕ) (h : a ≡ b [ZMOD n]) : a ^ m ≡ b ^ m [ZMOD n]

Full source

@[gcongr] 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, pow_succ]
  exact hd.mul h

Exponentiation Preserves Congruence Modulo $n$

Informal description

For any integers $a$, $b$, and $n$, and any natural number $m$, if $a \equiv b \pmod{n}$, then $a^m \equiv b^m \pmod{n}$.

Int.ModEq.of_mul_left theorem

(m : ℤ) (h : a ≡ b [ZMOD m * n]) : a ≡ b [ZMOD n]

Full source

lemma of_mul_left (m : ℤ) (h : a ≡ b [ZMOD m * n]) : a ≡ b [ZMOD n] := by
  rw [modEq_iff_dvd] at *; exact (dvd_mul_left n m).trans h

Congruence modulo a factor implies congruence modulo the base

Informal description

For integers $a$, $b$, $m$, and $n$, if $a \equiv b \pmod{m \cdot n}$, then $a \equiv b \pmod{n}$.

Int.ModEq.of_mul_right theorem

(m : ℤ) : a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n]

Full source

lemma of_mul_right (m : ℤ) : a ≡ b [ZMOD n * m] → a ≡ b [ZMOD n] :=
  mul_comm m n ▸ of_mul_left _

Congruence modulo a right factor implies congruence modulo the base

Informal description

For integers $a$, $b$, $m$, and $n$, if $a \equiv b \pmod{n \cdot m}$, then $a \equiv b \pmod{n}$.

Int.ModEq.cancel_right_div_gcd theorem

(hm : 0 < m) (h : a * c ≡ b * c [ZMOD m]) : a ≡ b [ZMOD m / gcd m c]

Full source

/-- 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
  rw [modEq_iff_dvd] at h ⊢
  refine Int.dvd_of_dvd_mul_right_of_gcd_one (?_ : m / d ∣ c / d * (b - a)) ?_
  · rw [mul_comm, ← Int.mul_ediv_assoc (b - a) gcd_dvd_right, Int.sub_mul]
    exact Int.ediv_dvd_ediv gcd_dvd_left h
  · rw [gcd_div gcd_dvd_left gcd_dvd_right, natAbs_natCast,
      Nat.div_self (gcd_pos_of_ne_zero_left c hm.ne')]

Congruence Cancellation: $a \cdot c \equiv b \cdot c \pmod{m}$ implies $a \equiv b \pmod{m / \gcd(m, c)}$

Informal description

For integers $a$, $b$, $c$, and $m$ with $m > 0$, if $a \cdot c \equiv b \cdot c \pmod{m}$, then $a \equiv b \pmod{m / \gcd(m, c)}$.

Int.ModEq.cancel_left_div_gcd theorem

(hm : 0 < m) (h : c * a ≡ c * b [ZMOD m]) : a ≡ b [ZMOD m / gcd m c]

Full source

/-- 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

Congruence Cancellation: $c \cdot a \equiv c \cdot b \pmod{m}$ implies $a \equiv b \pmod{m / \gcd(m, c)}$

Informal description

For integers $a$, $b$, $c$, and $m$ with $m > 0$, if $c \cdot a \equiv c \cdot b \pmod{m}$, then $a \equiv b \pmod{m / \gcd(m, c)}$.

Int.ModEq.of_div theorem

(h : a / c ≡ b / c [ZMOD m / c]) (ha : c ∣ a) (ha : c ∣ b) (ha : c ∣ m) : a ≡ b [ZMOD m]

Full source

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 convert h.mul_left' <;> rwa [Int.mul_ediv_cancel']

Congruence Lifting from Quotient Modulo Scaled Divisor

Informal description

For integers $a$, $b$, $c$, and $m$ with $c$ dividing $a$, $b$, and $m$, if $a/c \equiv b/c \pmod{m/c}$, then $a \equiv b \pmod{m}$.

Int.modEq_one theorem

: a ≡ b [ZMOD 1]

Full source

theorem modEq_one : a ≡ b [ZMOD 1] :=
  modEq_of_dvd (one_dvd _)

Congruence Modulo One Holds for All Integers

Informal description

For any integers $a$ and $b$, the congruence $a \equiv b \pmod{1}$ holds.

Int.modEq_sub theorem

(a b : ℤ) : a ≡ b [ZMOD a - b]

Full source

theorem modEq_sub (a b : ℤ) : a ≡ b [ZMOD a - b] :=
  (modEq_of_dvd dvd_rfl).symm

Congruence Modulo Difference: $a \equiv b \pmod{a - b}$

Informal description

For any integers $a$ and $b$, the congruence $a \equiv b \pmod{a - b}$ holds.

Int.modEq_zero_iff theorem

: a ≡ b [ZMOD 0] ↔ a = b

Full source

@[simp]
theorem modEq_zero_iff : a ≡ b [ZMOD 0]a ≡ b [ZMOD 0] ↔ a = b := by rw [ModEq, emod_zero, emod_zero]

Congruence Modulo Zero iff Equality

Informal description

For integers $a$ and $b$, the congruence $a \equiv b \pmod{0}$ holds if and only if $a = b$.

Int.add_modEq_left theorem

: n + a ≡ a [ZMOD n]

Full source

@[simp]
theorem add_modEq_left : n + a ≡ a [ZMOD n] := ModEq.symm <| modEq_iff_dvd.2 <| by simp

Left Addition Preserves Congruence Modulo $n$

Informal description

For any integers $a$ and $n$, the congruence $n + a \equiv a \pmod{n}$ holds.

Int.add_modEq_right theorem

: a + n ≡ a [ZMOD n]

Full source

@[simp]
theorem add_modEq_right : a + n ≡ a [ZMOD n] := ModEq.symm <| modEq_iff_dvd.2 <| by simp

Right Addition Preserves Congruence Modulo $n$

Informal description

For any integers $a$ and $n$, the congruence $a + n \equiv a \pmod{n}$ holds.

Int.modEq_and_modEq_iff_modEq_mul theorem

{a b m n : ℤ} (hmn : m.natAbs.Coprime n.natAbs) : a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n]

Full source

theorem modEq_and_modEq_iff_modEq_mul {a b m n : ℤ} (hmn : m.natAbs.Coprime n.natAbs) :
    a ≡ b [ZMOD m]a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n]a ≡ b [ZMOD m] ∧ a ≡ b [ZMOD n] ↔ a ≡ b [ZMOD m * n] :=
  ⟨fun h => by
    rw [modEq_iff_dvd, modEq_iff_dvd] at h
    rw [modEq_iff_dvd, ← natAbs_dvd, ← dvd_natAbs, natCast_dvd_natCast, natAbs_mul]
    refine hmn.mul_dvd_of_dvd_of_dvd ?_ ?_ <;>
      rw [← natCast_dvd_natCast, natAbs_dvd, dvd_natAbs] <;>
      tauto,
    fun h => ⟨h.of_mul_right _, h.of_mul_left _⟩⟩

Chinese Remainder Theorem for Integer Congruences with Coprime Moduli

Informal description

For integers $a, b, m, n$ with $\gcd(|m|, |n|) = 1$, the following are equivalent: 1. $a \equiv b \pmod{m}$ and $a \equiv b \pmod{n}$ 2. $a \equiv b \pmod{m \cdot n}$

Int.gcd_a_modEq theorem

(a b : ℕ) : (a : ℤ) * Nat.gcdA a b ≡ Nat.gcd a b [ZMOD b]

Full source

theorem gcd_a_modEq (a b : ℕ) : (a : ℤ) * Nat.gcdA a b ≡ Nat.gcd a b [ZMOD b] := by
  rw [← add_zero ((a : ℤ) * _), Nat.gcd_eq_gcd_ab]
  exact (dvd_mul_right _ _).zero_modEq_int.add_left _

Congruence of Bézout's coefficient: $a \cdot \text{gcdA}(a, b) \equiv \gcd(a, b) \pmod{b}$

Informal description

For any natural numbers $a$ and $b$, the integer $a \cdot \text{gcdA}(a, b)$ is congruent to $\gcd(a, b)$ modulo $b$, i.e., \[ a \cdot \text{gcdA}(a, b) \equiv \gcd(a, b) \pmod{b}. \] Here, $\text{gcdA}(a, b)$ is the first coefficient in Bézout's identity for $a$ and $b$.

Int.modEq_add_fac theorem

{a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a + n * c ≡ b [ZMOD n]

Full source

theorem modEq_add_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a + n * c ≡ b [ZMOD n] :=
  calc
    a + n * c ≡ b + n * c [ZMOD n] := ha.add_right _
    _ ≡ b + 0 [ZMOD n]calc
    a + n * c ≡ b + n * c [ZMOD n] := ha.add_right _
    _ ≡ b + 0 [ZMOD n] := (dvd_mul_right _ _).modEq_zero_int.add_left _
    _ ≡ b [ZMOD n] := by rw [add_zero]

Congruence Preservation under Addition of Multiple of Modulus

Informal description

For any integers $a$, $b$, $n$, and $c$, if $a \equiv b \pmod{n}$, then $a + n \cdot c \equiv b \pmod{n}$.

Int.modEq_sub_fac theorem

{a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a - n * c ≡ b [ZMOD n]

Full source

theorem modEq_sub_fac {a b n : ℤ} (c : ℤ) (ha : a ≡ b [ZMOD n]) : a - n * c ≡ b [ZMOD n] := by
  convert Int.modEq_add_fac (-c) ha using 1; rw [Int.mul_neg, sub_eq_add_neg]

Congruence Preservation under Subtraction of Multiple of Modulus

Informal description

For any integers $a$, $b$, $n$, and $c$, if $a \equiv b \pmod{n}$, then $a - n \cdot c \equiv b \pmod{n}$.

Int.modEq_add_fac_self theorem

{a t n : ℤ} : a + n * t ≡ a [ZMOD n]

Full source

theorem modEq_add_fac_self {a t n : ℤ} : a + n * t ≡ a [ZMOD n] :=
  modEq_add_fac _ ModEq.rfl

Congruence under Addition of Multiple of Modulus: $a + n \cdot t \equiv a \pmod{n}$

Informal description

For any integers $a$, $t$, and $n$, the congruence relation $a + n \cdot t \equiv a \pmod{n}$ holds.

Int.mod_coprime theorem

{a b : ℕ} (hab : Nat.Coprime a b) : ∃ y : ℤ, a * y ≡ 1 [ZMOD b]

Full source

theorem mod_coprime {a b : ℕ} (hab : Nat.Coprime a b) : ∃ y : ℤ, a * y ≡ 1 [ZMOD b] :=
  ⟨Nat.gcdA a b,
    have hgcd : Nat.gcd a b = 1 := Nat.Coprime.gcd_eq_one hab
    calc
      ↑a * Nat.gcdA a b ≡ ↑a * Nat.gcdA a b + ↑b * Nat.gcdB a b [ZMOD ↑b] :=
        ModEq.symm <| modEq_add_fac _ <| ModEq.refl _
      _ ≡ 1 [ZMOD ↑b] := by rw [← Nat.gcd_eq_gcd_ab, hgcd]; rfl
      ⟩

Existence of Modular Inverse for Coprime Integers

Informal description

For any natural numbers $a$ and $b$ that are coprime (i.e., $\gcd(a, b) = 1$), there exists an integer $y$ such that $a \cdot y \equiv 1 \pmod{b}$.

Int.existsUnique_equiv theorem

(a : ℤ) {b : ℤ} (hb : 0 < b) : ∃ z : ℤ, 0 ≤ z ∧ z < b ∧ z ≡ a [ZMOD b]

Full source

theorem existsUnique_equiv (a : ℤ) {b : ℤ} (hb : 0 < b) :
    ∃ z : ℤ, 0 ≤ z ∧ z < b ∧ z ≡ a [ZMOD b] :=
  ⟨a % b, emod_nonneg _ (ne_of_gt hb),
    by
      have : a % b < |b| := emod_lt_abs _ (ne_of_gt hb)
      rwa [abs_of_pos hb] at this, by simp [ModEq]⟩

Existence and Uniqueness of Integer Representative in $[0, b)$ Modulo $b$

Informal description

For any integer $a$ and any positive integer $b$, there exists a unique integer $z$ such that $0 \leq z < b$ and $z \equiv a \pmod{b}$.

Int.existsUnique_equiv_nat theorem

(a : ℤ) {b : ℤ} (hb : 0 < b) : ∃ z : ℕ, ↑z < b ∧ ↑z ≡ a [ZMOD b]

Full source

theorem existsUnique_equiv_nat (a : ℤ) {b : ℤ} (hb : 0 < b) : ∃ z : ℕ, ↑z < b ∧ ↑z ≡ a [ZMOD b] :=
  let ⟨z, hz1, hz2, hz3⟩ := existsUnique_equiv a hb
  ⟨z.natAbs, by
    constructor <;> rw [natAbs_of_nonneg hz1] <;> assumption⟩

Existence and Uniqueness of Natural Number Representative in $[0, b)$ Modulo $b$

Informal description

For any integer $a$ and any positive integer $b$, there exists a unique natural number $z$ such that $z < b$ and $z \equiv a \pmod{b}$.

Int.mod_mul_right_mod theorem

(a b c : ℤ) : a % (b * c) % b = a % b

Full source

theorem mod_mul_right_mod (a b c : ℤ) : a % (b * c) % b = a % b :=
  (mod_modEq _ _).of_mul_right _

Nested Remainder Identity: $(a \ \% \ (b \cdot c)) \ \% \ b = a \ \% \ b$

Informal description

For any integers $a$, $b$, and $c$, the remainder of $a$ modulo $b \cdot c$ taken modulo $b$ is equal to the remainder of $a$ modulo $b$, i.e., $(a \ \% \ (b \cdot c)) \ \% \ b = a \ \% \ b$.

Int.mod_mul_left_mod theorem

(a b c : ℤ) : a % (b * c) % c = a % c

Full source

theorem mod_mul_left_mod (a b c : ℤ) : a % (b * c) % c = a % c :=
  (mod_modEq _ _).of_mul_left _

Nested Remainder Identity: $(a \% (b \cdot c)) \% c = a \% c$

Informal description

For any integers $a$, $b$, and $c$, the remainder of $a$ modulo $b \cdot c$ taken modulo $c$ is equal to the remainder of $a$ modulo $c$, i.e., $(a \% (b \cdot c)) \% c = a \% c$.

Tags