Mathlib.Data.Nat.ModEq

Nat.ModEq definition

(n a b : ℕ)

Full source

/-- Modular equality. `n.ModEq a b`, or `a ≡ b [MOD n]`, means that `a - b` is a multiple of `n`. -/
def ModEq (n a b : ℕ) :=
  a % n = b % n

Congruence modulo $ n $

Informal description

For natural numbers $ n, a, b $, the relation $ a \equiv b \pmod{n} $ holds if and only if $ a $ and $ b $ have the same remainder when divided by $ n $. Equivalently, $ a - b $ is divisible by $ n $.

Nat.term_≡_[MOD_] definition

: Lean.TrailingParserDescr✝

Full source

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

Congruence modulo n notation

Informal description

The notation `a ≡ b [MOD n]` represents the equivalence relation `ModEq n a b`, which means that the natural numbers `a` and `b` are congruent modulo `n`, i.e., `a % n = b % n`.

Nat.instDecidableModEq instance

: Decidable (ModEq n a b)

Full source

instance : Decidable (ModEq n a b) := inferInstanceAs <| Decidable (a % n = b % n)

Decidability of Congruence Modulo $ n $

Informal description

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

Nat.ModEq.refl theorem

(a : ℕ) : a ≡ a [MOD n]

Full source

@[refl]
protected theorem refl (a : ℕ) : a ≡ a [MOD n] := rfl

Reflexivity of Congruence Modulo $n$

Informal description

For any natural number $a$, we have $a \equiv a \pmod{n}$ (i.e., $a$ is congruent to itself modulo $n$).

Nat.ModEq.rfl theorem

: a ≡ a [MOD n]

Full source

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

Reflexivity of Congruence Modulo $n$

Informal description

For any natural number $a$, we have $a \equiv a \pmod{n}$ (i.e., $a$ is congruent to itself modulo $n$).

Nat.ModEq.instIsRefl instance

: IsRefl _ (ModEq n)

Full source

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

Reflexivity of Congruence Modulo $n$

Informal description

For any natural number $n$, the congruence relation modulo $n$ is reflexive. That is, for any natural number $a$, we have $a \equiv a \pmod{n}$.

Nat.ModEq.symm theorem

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

Full source

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

Symmetry of Congruence Modulo $ n $

Informal description

For any natural numbers $ a, b, n $, if $ a \equiv b \pmod{n} $, then $ b \equiv a \pmod{n} $.

Nat.ModEq.trans theorem

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

Full source

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

Transitivity of Congruence Modulo $n$

Informal description

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

Nat.ModEq.instTrans instance

: Trans (ModEq n) (ModEq n) (ModEq n)

Full source

instance : Trans (ModEq n) (ModEq n) (ModEq n) where
  trans := Nat.ModEq.trans

Transitivity of Congruence Modulo $n$

Informal description

The relation of congruence modulo $n$ on natural numbers is transitive. That is, for any natural numbers $a$, $b$, $c$, and $n$, if $a \equiv b \pmod{n}$ and $b \equiv c \pmod{n}$, then $a \equiv c \pmod{n}$.

Nat.ModEq.comm theorem

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

Full source

protected theorem comm : a ≡ b [MOD n]a ≡ b [MOD n] ↔ b ≡ a [MOD n] :=
  ⟨ModEq.symm, ModEq.symm⟩

Symmetry of Congruence Modulo $n$: $a \equiv b \pmod{n} \leftrightarrow b \equiv a \pmod{n}$

Informal description

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

Nat.modEq_zero_iff_dvd theorem

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

Full source

theorem modEq_zero_iff_dvd : a ≡ 0 [MOD n]a ≡ 0 [MOD n] ↔ n ∣ a := by rw [ModEq, zero_mod, dvd_iff_mod_eq_zero]

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

Informal description

For natural numbers $a$ and $n$, the congruence $a \equiv 0 \pmod{n}$ holds if and only if $n$ divides $a$.

Dvd.dvd.modEq_zero_nat theorem

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

Full source

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

Divisibility Implies Congruence to Zero Modulo $n$

Informal description

For any natural numbers $a$ and $n$, if $n$ divides $a$, then $a \equiv 0 \pmod{n}$.

Dvd.dvd.zero_modEq_nat theorem

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

Full source

theorem _root_.Dvd.dvd.zero_modEq_nat (h : n ∣ a) : 0 ≡ a [MOD n] :=
  h.modEq_zero_nat.symm

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

Informal description

For any natural numbers $a$ and $n$, if $n$ divides $a$, then $0 \equiv a \pmod{n}$.

Nat.modEq_iff_dvd theorem

: a ≡ b [MOD n] ↔ (n : ℤ) ∣ b - a

Full source

theorem modEq_iff_dvd : a ≡ b [MOD n]a ≡ b [MOD n] ↔ (n : ℤ) ∣ b - a := by
  rw [ModEq, eq_comm, ← Int.natCast_inj, Int.natCast_mod, Int.natCast_mod,
    Int.emod_eq_emod_iff_emod_sub_eq_zero, Int.dvd_iff_emod_eq_zero]

Congruence Modulo $n$ in Terms of Divisibility

Informal description

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

Nat.modEq_iff_dvd' theorem

(h : a ≤ b) : a ≡ b [MOD n] ↔ n ∣ b - a

Full source

/-- A variant of `modEq_iff_dvd` with `Nat` divisibility -/
theorem modEq_iff_dvd' (h : a ≤ b) : a ≡ b [MOD n]a ≡ b [MOD n] ↔ n ∣ b - a := by
  rw [modEq_iff_dvd, ← Int.natCast_dvd_natCast, Int.ofNat_sub h]

Congruence Modulo $n$ in Terms of Divisibility (Natural Numbers)

Informal description

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

Nat.mod_modEq theorem

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

Full source

theorem mod_modEq (a n) : a % n ≡ a [MOD n] :=
  mod_mod _ _

Congruence of Remainder Modulo $n$: $a \% n \equiv a \pmod{n}$

Informal description

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

Nat.ModEq.of_dvd theorem

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

Full source

lemma of_dvd (d : m ∣ n) (h : a ≡ b [MOD n]) : a ≡ b [MOD m] :=
  modEq_of_dvd <| Int.ofNat_dvd.mpr d |>.trans h.dvd

Congruence Preservation Under Divisor Relation: $a \equiv b \pmod{n}$ implies $a \equiv b \pmod{m}$ when $m \mid n$

Informal description

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

Nat.ModEq.mul_left' theorem

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

Full source

protected theorem mul_left' (c : ℕ) (h : a ≡ b [MOD n]) : c * a ≡ c * b [MOD c * n] := by
  unfold ModEq at *; rw [mul_mod_mul_left, mul_mod_mul_left, h]

Multiplication Preserves Congruence with Scaled Modulus

Informal description

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

Nat.ModEq.mul_left theorem

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

Full source

@[gcongr]
protected theorem mul_left (c : ℕ) (h : a ≡ b [MOD n]) : c * a ≡ c * b [MOD n] :=
  (h.mul_left' _).of_dvd (dvd_mul_left _ _)

Left Multiplication Preserves Congruence Modulo $n$

Informal description

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

Nat.ModEq.mul_right' theorem

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

Full source

protected theorem mul_right' (c : ℕ) (h : a ≡ b [MOD n]) : a * c ≡ b * c [MOD n * c] := by
  rw [mul_comm a, mul_comm b, mul_comm n]; exact h.mul_left' c

Right Multiplication Preserves Congruence with Scaled Modulus

Informal description

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

Nat.ModEq.mul_right theorem

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

Full source

@[gcongr]
protected theorem mul_right (c : ℕ) (h : a ≡ b [MOD n]) : a * c ≡ b * c [MOD n] := by
  rw [mul_comm a, mul_comm b]; exact h.mul_left c

Right Multiplication Preserves Congruence Modulo $n$

Informal description

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

Nat.ModEq.mul theorem

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

Full source

@[gcongr]
protected theorem mul (h₁ : a ≡ b [MOD n]) (h₂ : c ≡ d [MOD n]) : a * c ≡ b * d [MOD n] :=
  (h₂.mul_left _).trans (h₁.mul_right _)

Multiplication Preserves Congruence Modulo $n$

Informal description

For any natural numbers $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}$.

Nat.ModEq.pow theorem

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

Full source

@[gcongr]
protected theorem pow (m : ℕ) (h : a ≡ b [MOD n]) : a ^ m ≡ b ^ m [MOD n] := by
  induction m with
  | zero => rfl
  | succ d hd =>
    rw [Nat.pow_succ, Nat.pow_succ]
    exact hd.mul h

Exponentiation Preserves Congruence Modulo $n$

Informal description

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

Nat.ModEq.add theorem

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

Full source

@[gcongr]
protected theorem add (h₁ : a ≡ b [MOD n]) (h₂ : c ≡ d [MOD n]) : a + c ≡ b + d [MOD n] := by
  rw [modEq_iff_dvd, Int.natCast_add, Int.natCast_add, add_sub_add_comm]
  exact Int.dvd_add h₁.dvd h₂.dvd

Addition Preserves Congruence Modulo $n$

Informal description

For natural numbers $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}$.

Nat.ModEq.add_left theorem

(c : ℕ) (h : a ≡ b [MOD n]) : c + a ≡ c + b [MOD n]

Full source

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

Left Addition Preserves Congruence Modulo $n$

Informal description

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

Nat.ModEq.add_right theorem

(c : ℕ) (h : a ≡ b [MOD n]) : a + c ≡ b + c [MOD n]

Full source

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

Right Addition Preserves Congruence Modulo $n$

Informal description

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

Nat.ModEq.add_left_cancel theorem

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

Full source

protected theorem add_left_cancel (h₁ : a ≡ b [MOD n]) (h₂ : a + c ≡ b + d [MOD n]) :
    c ≡ d [MOD n] := by
  simp only [modEq_iff_dvd, Int.natCast_add] at *
  rw [add_sub_add_comm] at h₂
  convert Int.dvd_sub h₂ h₁ using 1
  rw [add_sub_cancel_left]

Left Cancellation Property of Congruence Modulo $n$

Informal description

For natural numbers $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}$.

Nat.ModEq.add_left_cancel' theorem

(c : ℕ) (h : c + a ≡ c + b [MOD n]) : a ≡ b [MOD n]

Full source

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

Left Cancellation of Addition in Congruence Modulo $n$

Informal description

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

Nat.ModEq.add_right_cancel theorem

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

Full source

protected theorem add_right_cancel (h₁ : c ≡ d [MOD n]) (h₂ : a + c ≡ b + d [MOD n]) :
    a ≡ b [MOD n] := by
  rw [add_comm a, add_comm b] at h₂
  exact h₁.add_left_cancel h₂

Right Cancellation Property of Congruence Modulo $n$

Informal description

For natural numbers $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}$.

Nat.ModEq.add_right_cancel' theorem

(c : ℕ) (h : a + c ≡ b + c [MOD n]) : a ≡ b [MOD n]

Full source

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

Right Cancellation of Addition in Congruence Modulo $n$

Informal description

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

Nat.ModEq.mul_left_cancel' theorem

{a b c m : ℕ} (hc : c ≠ 0) : c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m]

Full source

/-- Cancel left multiplication on both sides of the `≡` and in the modulus.

For cancelling left multiplication in the modulus, see `Nat.ModEq.of_mul_left`. -/
protected theorem mul_left_cancel' {a b c m : ℕ} (hc : c ≠ 0) :
    c * a ≡ c * b [MOD c * m] → a ≡ b [MOD m] := by
  simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.mul_sub]
  exact fun h => (Int.dvd_of_mul_dvd_mul_left (Int.ofNat_ne_zero.mpr hc) h)

Left Multiplication Cancellation in Congruence Modulo $n$

Informal description

For natural numbers $a, b, c, m$ with $c \neq 0$, if $c \cdot a \equiv c \cdot b \pmod{c \cdot m}$, then $a \equiv b \pmod{m}$.

Nat.ModEq.mul_left_cancel_iff' theorem

{a b c m : ℕ} (hc : c ≠ 0) : c * a ≡ c * b [MOD c * m] ↔ a ≡ b [MOD m]

Full source

protected theorem mul_left_cancel_iff' {a b c m : ℕ} (hc : c ≠ 0) :
    c * a ≡ c * b [MOD c * m]c * a ≡ c * b [MOD c * m] ↔ a ≡ b [MOD m] :=
  ⟨ModEq.mul_left_cancel' hc, ModEq.mul_left' _⟩

Equivalence of Congruences After Left Multiplication: $c \cdot a \equiv c \cdot b \pmod{c \cdot m} \leftrightarrow a \equiv b \pmod{m}$

Informal description

For natural numbers $a, b, c, m$ with $c \neq 0$, the congruence $c \cdot a \equiv c \cdot b \pmod{c \cdot m}$ holds if and only if $a \equiv b \pmod{m}$.

Nat.ModEq.mul_right_cancel' theorem

{a b c m : ℕ} (hc : c ≠ 0) : a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m]

Full source

/-- Cancel right multiplication on both sides of the `≡` and in the modulus.

For cancelling right multiplication in the modulus, see `Nat.ModEq.of_mul_right`. -/
protected theorem mul_right_cancel' {a b c m : ℕ} (hc : c ≠ 0) :
    a * c ≡ b * c [MOD m * c] → a ≡ b [MOD m] := by
  simp only [modEq_iff_dvd, Int.natCast_mul, ← Int.sub_mul]
  exact fun h => (Int.dvd_of_mul_dvd_mul_right (Int.ofNat_ne_zero.mpr hc) h)

Right Multiplication Cancellation in Congruence Modulo $n$

Informal description

For natural numbers $a, b, c, m$ with $c \neq 0$, if $a \cdot c \equiv b \cdot c \pmod{m \cdot c}$, then $a \equiv b \pmod{m}$.

Nat.ModEq.mul_right_cancel_iff' theorem

{a b c m : ℕ} (hc : c ≠ 0) : a * c ≡ b * c [MOD m * c] ↔ a ≡ b [MOD m]

Full source

protected theorem mul_right_cancel_iff' {a b c m : ℕ} (hc : c ≠ 0) :
    a * c ≡ b * c [MOD m * c]a * c ≡ b * c [MOD m * c] ↔ a ≡ b [MOD m] :=
  ⟨ModEq.mul_right_cancel' hc, ModEq.mul_right' _⟩

Right Multiplication Cancellation in Congruence Modulo $n$: $a \cdot c \equiv b \cdot c \pmod{m \cdot c} \leftrightarrow a \equiv b \pmod{m}$

Informal description

For natural numbers $a, b, c, m$ with $c \neq 0$, the congruence relation $a \cdot c \equiv b \cdot c \pmod{m \cdot c}$ holds if and only if $a \equiv b \pmod{m}$.

Nat.ModEq.of_mul_left theorem

(m : ℕ) (h : a ≡ b [MOD m * n]) : a ≡ b [MOD n]

Full source

/-- Cancel left multiplication in the modulus.

For cancelling left multiplication on both sides of the `≡`, see `nat.modeq.mul_left_cancel'`. -/
lemma of_mul_left (m : ℕ) (h : a ≡ b [MOD m * n]) : a ≡ b [MOD n] := by
  rw [modEq_iff_dvd] at *
  exact (dvd_mul_left (n : ℤ) (m : ℤ)).trans h

Congruence modulo $m \cdot n$ implies congruence modulo $n$

Informal description

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

Nat.ModEq.of_mul_right theorem

(m : ℕ) : a ≡ b [MOD n * m] → a ≡ b [MOD n]

Full source

/-- Cancel right multiplication in the modulus.

For cancelling right multiplication on both sides of the `≡`, see `nat.modeq.mul_right_cancel'`. -/
lemma of_mul_right (m : ℕ) : a ≡ b [MOD n * m] → a ≡ b [MOD n] := mul_comm m n ▸ of_mul_left _

Congruence modulo $n \cdot m$ implies congruence modulo $n$

Informal description

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

Nat.ModEq.of_div theorem

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

Full source

theorem of_div (h : a / c ≡ b / c [MOD m / c]) (ha : c ∣ a) (ha : c ∣ b) (ha : c ∣ m) :
    a ≡ b [MOD m] := by convert h.mul_left' c <;> rwa [Nat.mul_div_cancel']

Congruence Preservation under Division by Common Factor

Informal description

For natural numbers $a$, $b$, $c$, and $m$, if $c$ divides $a$, $b$, and $m$, and $a/c \equiv b/c \pmod{m/c}$, then $a \equiv b \pmod{m}$.

Nat.modEq_sub theorem

(h : b ≤ a) : a ≡ b [MOD a - b]

Full source

lemma modEq_sub (h : b ≤ a) : a ≡ b [MOD a - b] := (modEq_of_dvd <| by rw [Int.ofNat_sub h]).symm

Congruence of Natural Numbers Modulo Their Difference

Informal description

For any natural numbers $a$ and $b$ such that $b \leq a$, we have $a \equiv b \pmod{a - b}$.

Nat.modEq_one theorem

: a ≡ b [MOD 1]

Full source

lemma modEq_one : a ≡ b [MOD 1] := modEq_of_dvd <| one_dvd _

All Numbers Congruent Modulo 1

Informal description

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

Nat.modEq_zero_iff theorem

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

Full source

@[simp] lemma modEq_zero_iff : a ≡ b [MOD 0]a ≡ b [MOD 0] ↔ a = b := by rw [ModEq, mod_zero, mod_zero]

Congruence Modulo Zero Characterizes Equality

Informal description

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

Nat.add_modEq_left theorem

: n + a ≡ a [MOD n]

Full source

@[simp] lemma add_modEq_left : n + a ≡ a [MOD n] := by rw [ModEq, add_mod_left]

Congruence of Sum with Identity Modulo $n$: $n + a \equiv a \pmod{n}$

Informal description

For any natural numbers $n$ and $a$, the sum $n + a$ is congruent to $a$ modulo $n$, i.e., $n + a \equiv a \pmod{n}$.

Nat.add_modEq_right theorem

: a + n ≡ a [MOD n]

Full source

@[simp] lemma add_modEq_right : a + n ≡ a [MOD n] := by rw [ModEq, add_mod_right]

Right Addition Preserves Congruence Modulo $n$

Informal description

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

Nat.ModEq.le_of_lt_add theorem

(h1 : a ≡ b [MOD m]) (h2 : a < b + m) : a ≤ b

Full source

theorem le_of_lt_add (h1 : a ≡ b [MOD m]) (h2 : a < b + m) : a ≤ b :=
  (le_total a b).elim id fun h3 =>
    Nat.le_of_sub_eq_zero
      (eq_zero_of_dvd_of_lt ((modEq_iff_dvd' h3).mp h1.symm) (by omega))

Upper Bound from Congruence and Inequality Modulo $m$

Informal description

For any natural numbers $a$, $b$, and $m$, if $a \equiv b \pmod{m}$ and $a < b + m$, then $a \leq b$.

Nat.ModEq.add_le_of_lt theorem

(h1 : a ≡ b [MOD m]) (h2 : a < b) : a + m ≤ b

Full source

theorem add_le_of_lt (h1 : a ≡ b [MOD m]) (h2 : a < b) : a + m ≤ b :=
  le_of_lt_add (add_modEq_right.trans h1) (by omega)

Lower Bound from Congruence and Strict Inequality Modulo $m$

Informal description

For any natural numbers $a$, $b$, and $m$, if $a \equiv b \pmod{m}$ and $a < b$, then $a + m \leq b$.

Nat.ModEq.dvd_iff theorem

(h : a ≡ b [MOD m]) (hdm : d ∣ m) : d ∣ a ↔ d ∣ b

Full source

theorem dvd_iff (h : a ≡ b [MOD m]) (hdm : d ∣ m) : d ∣ ad ∣ a ↔ d ∣ b := by
  simp only [← modEq_zero_iff_dvd]
  replace h := h.of_dvd hdm
  exact ⟨h.symm.trans, h.trans⟩

Divisibility Equivalence under Congruence: $d \mid a \leftrightarrow d \mid b$ when $a \equiv b \pmod{m}$ and $d \mid m$

Informal description

For any natural numbers $a$, $b$, $m$, and $d$ such that $d$ divides $m$, if $a \equiv b \pmod{m}$, then $d$ divides $a$ if and only if $d$ divides $b$.

Nat.ModEq.gcd_eq theorem

(h : a ≡ b [MOD m]) : gcd a m = gcd b m

Full source

theorem gcd_eq (h : a ≡ b [MOD m]) : gcd a m = gcd b m := by
  have h1 := gcd_dvd_right a m
  have h2 := gcd_dvd_right b m
  exact
    dvd_antisymm (dvd_gcd ((h.dvd_iff h1).mp (gcd_dvd_left a m)) h1)
      (dvd_gcd ((h.dvd_iff h2).mpr (gcd_dvd_left b m)) h2)

Invariance of GCD under Congruence: $\gcd(a, m) = \gcd(b, m)$ when $a \equiv b \pmod{m}$

Informal description

For any natural numbers $a$, $b$, and $m$, if $a \equiv b \pmod{m}$, then the greatest common divisor of $a$ and $m$ is equal to the greatest common divisor of $b$ and $m$, i.e., $\gcd(a, m) = \gcd(b, m)$.

Nat.ModEq.cancel_left_div_gcd theorem

(hm : 0 < m) (h : c * a ≡ c * b [MOD m]) : a ≡ b [MOD 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` -/
lemma cancel_left_div_gcd (hm : 0 < m) (h : c * a ≡ c * b [MOD m]) :  a ≡ b [MOD m / gcd m c] := by
  let d := gcd m c
  have hmd := gcd_dvd_left m c
  have hcd := gcd_dvd_right m c
  rw [modEq_iff_dvd]
  refine @Int.dvd_of_dvd_mul_right_of_gcd_one (m / d) (c / d) (b - a) ?_ ?_
  · show (m / d : ℤ) ∣ c / d * (b - a)
    rw [mul_comm, ← Int.mul_ediv_assoc (b - a) (Int.natCast_dvd_natCast.mpr hcd), mul_comm]
    apply Int.ediv_dvd_ediv (Int.natCast_dvd_natCast.mpr hmd)
    rw [Int.mul_sub]
    exact modEq_iff_dvd.mp h
  · show Int.gcd (m / d) (c / d) = 1
    simp only [d, ← Int.natCast_div, Int.gcd_natCast_natCast (m / d) (c / d),
      gcd_div hmd hcd, Nat.div_self (gcd_pos_of_pos_left c hm)]

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

Informal description

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

Nat.ModEq.cancel_right_div_gcd theorem

(hm : 0 < m) (h : a * c ≡ b * c [MOD m]) : a ≡ b [MOD 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` -/
lemma cancel_right_div_gcd (hm : 0 < m) (h : a * c ≡ b * c [MOD m]) : a ≡ b [MOD m / gcd m c] := by
  apply cancel_left_div_gcd hm
  simpa [mul_comm] using h

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

Informal description

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

Nat.ModEq.cancel_left_div_gcd' theorem

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

Full source

lemma cancel_left_div_gcd' (hm : 0 < m) (hcd : c ≡ d [MOD m]) (h : c * a ≡ d * b [MOD m]) :
    a ≡ b [MOD m / gcd m c] :=
  (h.trans <| hcd.symm.mul_right b).cancel_left_div_gcd hm

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

Informal description

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

Nat.ModEq.cancel_right_div_gcd' theorem

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

Full source

lemma cancel_right_div_gcd' (hm : 0 < m) (hcd : c ≡ d [MOD m]) (h : a * c ≡ b * d [MOD m]) :
    a ≡ b [MOD m / gcd m c] :=
  (h.trans <| hcd.symm.mul_left b).cancel_right_div_gcd hm

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

Informal description

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

Nat.ModEq.cancel_left_of_coprime theorem

(hmc : gcd m c = 1) (h : c * a ≡ c * b [MOD m]) : a ≡ b [MOD m]

Full source

/-- A common factor that's coprime with the modulus can be cancelled from a `ModEq` -/
lemma cancel_left_of_coprime (hmc : gcd m c = 1) (h : c * a ≡ c * b [MOD m]) : a ≡ b [MOD m] := by
  rcases m.eq_zero_or_pos with (rfl | hm)
  · simp only [gcd_zero_left] at hmc
    simp only [gcd_zero_left, hmc, one_mul, modEq_zero_iff] at h
    subst h
    rfl
  simpa [hmc] using h.cancel_left_div_gcd hm

Congruence Cancellation with Coprime Factor: $c \cdot a \equiv c \cdot b \pmod{m}$ implies $a \equiv b \pmod{m}$ when $\gcd(m, c) = 1$

Informal description

For natural numbers $m$, $a$, $b$, and $c$, if $\gcd(m, c) = 1$ and $c \cdot a \equiv c \cdot b \pmod{m}$, then $a \equiv b \pmod{m}$.

Nat.ModEq.cancel_right_of_coprime theorem

(hmc : gcd m c = 1) (h : a * c ≡ b * c [MOD m]) : a ≡ b [MOD m]

Full source

/-- A common factor that's coprime with the modulus can be cancelled from a `ModEq` -/
lemma cancel_right_of_coprime (hmc : gcd m c = 1) (h : a * c ≡ b * c [MOD m]) : a ≡ b [MOD m] :=
  cancel_left_of_coprime hmc <| by simpa [mul_comm] using h

Right cancellation in congruences with coprime factor: $a \cdot c \equiv b \cdot c \pmod{m} \Rightarrow a \equiv b \pmod{m}$ when $\gcd(m, c) = 1$

Informal description

For natural numbers $a, b, c, m$ with $\gcd(m, c) = 1$, if $a \cdot c \equiv b \cdot c \pmod{m}$, then $a \equiv b \pmod{m}$.

Nat.chineseRemainder' definition

(h : a ≡ b [MOD gcd n m]) : { k // k ≡ a [MOD n] ∧ k ≡ b [MOD m] }

Full source

/-- The natural number less than `lcm n m` congruent to `a` mod `n` and `b` mod `m` -/
def chineseRemainder' (h : a ≡ b [MOD gcd n m]) : { k // k ≡ a [MOD n] ∧ k ≡ b [MOD m] } :=
  if hn : n = 0 then ⟨a, by
    rw [hn, gcd_zero_left] at h; constructor
    · rfl
    · exact h⟩
  else
    if hm : m = 0 then ⟨b, by
      rw [hm, gcd_zero_right] at h; constructor
      · exact h.symm
      · rfl⟩
    else
      ⟨let (c, d) := xgcd n m; Int.toNat ((n * c * b + m * d * a) / gcd n m % lcm n m), by
        rw [xgcd_val]
        dsimp
        rw [modEq_iff_dvd, modEq_iff_dvd,
          Int.toNat_of_nonneg (Int.emod_nonneg _ (Int.natCast_ne_zero.2 (lcm_ne_zero hn hm)))]
        have hnonzero : (gcd n m : ℤ) ≠ 0 := by
          norm_cast
          rw [Nat.gcd_eq_zero_iff, not_and]
          exact fun _ => hm
        have hcoedvd : ∀ t, (gcd n m : ℤ) ∣ t * (b - a) := fun t => h.dvd.mul_left _
        have := gcd_eq_gcd_ab n m
        constructor <;> rw [Int.emod_def, ← sub_add] <;>
            refine Int.dvd_add ?_ (dvd_mul_of_dvd_left ?_ _) <;>
          try norm_cast
        · rw [← sub_eq_iff_eq_add'] at this
          rw [← this, Int.sub_mul, ← add_sub_assoc, add_comm, add_sub_assoc, ← Int.mul_sub,
            Int.add_ediv_of_dvd_left, Int.mul_ediv_cancel_left _ hnonzero,
            Int.mul_ediv_assoc _ h.dvd, ← sub_sub, sub_self, zero_sub, Int.dvd_neg, mul_assoc]
          · exact dvd_mul_right _ _
          norm_cast
          exact dvd_mul_right _ _
        · exact dvd_lcm_left n m
        · rw [← sub_eq_iff_eq_add] at this
          rw [← this, Int.sub_mul, sub_add, ← Int.mul_sub, Int.sub_ediv_of_dvd,
            Int.mul_ediv_cancel_left _ hnonzero, Int.mul_ediv_assoc _ h.dvd, ← sub_add, sub_self,
            zero_add, mul_assoc]
          · exact dvd_mul_right _ _
          · exact hcoedvd _
        · exact dvd_lcm_right n m⟩

Chinese Remainder Theorem (constructive version)

Informal description

Given natural numbers $ n, m, a, b $ and a proof $ h $ that $ a \equiv b \pmod{\gcd(n, m)} $, the function returns a natural number $ k $ such that $ k \equiv a \pmod{n} $ and $ k \equiv b \pmod{m} $. The number $ k $ is constructed using the extended GCD algorithm and is taken modulo the least common multiple of $ n $ and $ m $.

Nat.chineseRemainder definition

(co : n.Coprime m) (a b : ℕ) : { k // k ≡ a [MOD n] ∧ k ≡ b [MOD m] }

Full source

/-- The natural number less than `n*m` congruent to `a` mod `n` and `b` mod `m` -/
def chineseRemainder (co : n.Coprime m) (a b : ℕ) : { k // k ≡ a [MOD n] ∧ k ≡ b [MOD m] } :=
  chineseRemainder' (by convert @modEq_one a b)

Chinese Remainder Theorem for Coprime Moduli

Informal description

Given coprime natural numbers $ n $ and $ m $, and natural numbers $ a $ and $ b $, the function returns a natural number $ k $ such that $ k \equiv a \pmod{n} $ and $ k \equiv b \pmod{m} $. The number $ k $ is constructed using the extended GCD algorithm and is taken modulo $ n \times m $.

Nat.chineseRemainder'_lt_lcm theorem

(h : a ≡ b [MOD gcd n m]) (hn : n ≠ 0) (hm : m ≠ 0) : ↑(chineseRemainder' h) < lcm n m

Full source

theorem chineseRemainder'_lt_lcm (h : a ≡ b [MOD gcd n m]) (hn : n ≠ 0) (hm : m ≠ 0) :
    ↑(chineseRemainder' h) < lcm n m := by
  dsimp only [chineseRemainder']
  rw [dif_neg hn, dif_neg hm, Subtype.coe_mk, xgcd_val, ← Int.toNat_natCast (lcm n m)]
  have lcm_pos := Int.natCast_pos.mpr (Nat.pos_of_ne_zero (lcm_ne_zero hn hm))
  exact (Int.toNat_lt_toNat lcm_pos).mpr (Int.emod_lt_of_pos _ lcm_pos)

Bound on Chinese Remainder Solution: $k < \text{lcm}(n, m)$

Informal description

Given natural numbers $a, b, n, m$ with $n \neq 0$ and $m \neq 0$, and a proof that $a \equiv b \pmod{\gcd(n, m)}$, the solution $k$ obtained from the Chinese remainder theorem satisfies $k < \text{lcm}(n, m)$.

Nat.chineseRemainder_lt_mul theorem

(co : n.Coprime m) (a b : ℕ) (hn : n ≠ 0) (hm : m ≠ 0) : ↑(chineseRemainder co a b) < n * m

Full source

theorem chineseRemainder_lt_mul (co : n.Coprime m) (a b : ℕ) (hn : n ≠ 0) (hm : m ≠ 0) :
    ↑(chineseRemainder co a b) < n * m :=
  lt_of_lt_of_le (chineseRemainder'_lt_lcm _ hn hm) (le_of_eq co.lcm_eq_mul)

Bound on Chinese Remainder Solution: $k < n \cdot m$ for Coprime Moduli

Informal description

For any coprime natural numbers $n$ and $m$ with $n \neq 0$ and $m \neq 0$, and any natural numbers $a$ and $b$, the solution $k$ obtained from the Chinese Remainder Theorem satisfies $k < n \cdot m$.

Nat.mod_lcm theorem

(hn : a ≡ b [MOD n]) (hm : a ≡ b [MOD m]) : a ≡ b [MOD lcm n m]

Full source

theorem mod_lcm (hn : a ≡ b [MOD n]) (hm : a ≡ b [MOD m]) : a ≡ b [MOD lcm n m] :=
  Nat.modEq_iff_dvd.mpr <| Int.coe_lcm_dvd (Nat.modEq_iff_dvd.mp hn) (Nat.modEq_iff_dvd.mp hm)

Congruence Modulo Least Common Multiple: $a \equiv b \pmod{n} \land a \equiv b \pmod{m} \to a \equiv b \pmod{\text{lcm}(n,m)}$

Informal description

For any natural numbers $a$, $b$, $n$, and $m$, if $a \equiv b \pmod{n}$ and $a \equiv b \pmod{m}$, then $a \equiv b \pmod{\text{lcm}(n,m)}$.

Nat.chineseRemainder_modEq_unique theorem

 (co : n.Coprime m) {a b z} (hzan : z ≡ a [MOD n]) (hzbm : z ≡ b [MOD m]) : z ≡ chineseRemainder co a b [MOD n * m]

Full source

theorem chineseRemainder_modEq_unique (co : n.Coprime m) {a b z}
    (hzan : z ≡ a [MOD n]) (hzbm : z ≡ b [MOD m]) : z ≡ chineseRemainder co a b [MOD n*m] := by
  simpa [Nat.Coprime.lcm_eq_mul co] using
    mod_lcm (hzan.trans ((chineseRemainder co a b).prop.1).symm)
      (hzbm.trans ((chineseRemainder co a b).prop.2).symm)

Uniqueness of Chinese Remainder Solution Modulo Product of Coprimes

Informal description

Given coprime natural numbers $n$ and $m$, and natural numbers $a$, $b$, and $z$ such that $z \equiv a \pmod{n}$ and $z \equiv b \pmod{m}$, then $z$ is congruent modulo $n \cdot m$ to the solution $k$ provided by the Chinese Remainder Theorem (i.e., $z \equiv k \pmod{n \cdot m}$ where $k$ satisfies $k \equiv a \pmod{n}$ and $k \equiv b \pmod{m}$).

Nat.modEq_and_modEq_iff_modEq_mul theorem

{a b m n : ℕ} (hmn : m.Coprime n) : a ≡ b [MOD m] ∧ a ≡ b [MOD n] ↔ a ≡ b [MOD m * n]

Full source

theorem modEq_and_modEq_iff_modEq_mul {a b m n : ℕ} (hmn : m.Coprime n) :
    a ≡ b [MOD m]a ≡ b [MOD m] ∧ a ≡ b [MOD n]a ≡ b [MOD m] ∧ a ≡ b [MOD n] ↔ a ≡ b [MOD m * n] :=
  ⟨fun h => by
    rw [Nat.modEq_iff_dvd, Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.natCast_dvd_natCast,
      ← Int.dvd_natAbs, Int.natCast_dvd_natCast] at h
    rw [Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]
    exact hmn.mul_dvd_of_dvd_of_dvd h.1 h.2,
   fun h => ⟨h.of_mul_right _, h.of_mul_left _⟩⟩

Chinese Remainder Theorem: $a \equiv b \pmod{m} \land a \equiv b \pmod{n} \leftrightarrow a \equiv b \pmod{mn}$ for coprime $m,n$

Informal description

For any natural numbers $a, b, m, n$ with $m$ and $n$ coprime, the following equivalence holds: $a \equiv b \pmod{m}$ and $a \equiv b \pmod{n}$ if and only if $a \equiv b \pmod{m \cdot n}$.

Nat.coprime_of_mul_modEq_one theorem

(b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) : a.Coprime n

Full source

theorem coprime_of_mul_modEq_one (b : ℕ) {a n : ℕ} (h : a * b ≡ 1 [MOD n]) : a.Coprime n := by
  obtain ⟨g, hh⟩ := Nat.gcd_dvd_right a n
  rw [Nat.coprime_iff_gcd_eq_one, ← Nat.dvd_one, ← Nat.modEq_zero_iff_dvd]
  calc
    1 ≡ a * b [MOD a.gcd n] := (hh ▸ h).symm.of_mul_right g
    _ ≡ 0 * b [MOD a.gcd n] := (Nat.modEq_zero_iff_dvd.mpr (Nat.gcd_dvd_left _ _)).mul_right b
    _ = 0 := by rw [zero_mul]

Coprimality from Modular Inverse: $a \cdot b \equiv 1 \pmod{n} \Rightarrow \text{coprime}(a, n)$

Informal description

For any natural numbers $a$, $b$, and $n$, if $a \cdot b \equiv 1 \pmod{n}$, then $a$ and $n$ are coprime.

Nat.add_mod_add_ite theorem

(a b c : ℕ) : ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c

Full source

theorem add_mod_add_ite (a b c : ℕ) :
    ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c :=
  have : (a + b) % c = (a % c + b % c) % c := ((mod_modEq _ _).add <| mod_modEq _ _).symm
  if hc0 : c = 0 then by simp [hc0, Nat.mod_zero]
  else by
    rw [this]
    split_ifs with h
    · have h2 : (a % c + b % c) / c < 2 :=
        Nat.div_lt_of_lt_mul
          (by
            rw [mul_two]
            exact
              add_lt_add (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0))
                (Nat.mod_lt _ (Nat.pos_of_ne_zero hc0)))
      have h0 : 0 < (a % c + b % c) / c := Nat.div_pos h (Nat.pos_of_ne_zero hc0)
      rw [← @add_right_cancel_iff _ _ _ (c * ((a % c + b % c) / c)), add_comm _ c, add_assoc,
        mod_add_div, le_antisymm (le_of_lt_succ h2) h0, mul_one, add_comm]
    · rw [Nat.mod_eq_of_lt (lt_of_not_ge h), add_zero]

Modular Addition with Conditional Correction: $(a + b) \bmod c + \text{correction} = a \bmod c + b \bmod c$

Informal description

For any natural numbers $a$, $b$, and $c$, the sum of $(a + b) \bmod c$ and an additional term (which is $c$ if $c \leq (a \bmod c + b \bmod c)$, otherwise $0$) equals $a \bmod c + b \bmod c$. In other words: $$(a + b) \bmod c + \begin{cases} c & \text{if } c \leq a \bmod c + b \bmod c \\ 0 & \text{otherwise} \end{cases} = a \bmod c + b \bmod c$$

Nat.add_mod_of_add_mod_lt theorem

{a b c : ℕ} (hc : a % c + b % c < c) : (a + b) % c = a % c + b % c

Full source

theorem add_mod_of_add_mod_lt {a b c : ℕ} (hc : a % c + b % c < c) :
    (a + b) % c = a % c + b % c := by rw [← add_mod_add_ite, if_neg (not_le_of_lt hc), add_zero]

Modular Addition of Remainders When Sum is Less Than Divisor

Informal description

For any natural numbers $a$, $b$, and $c$ such that $a \bmod c + b \bmod c < c$, the remainder of the sum $a + b$ modulo $c$ equals the sum of the remainders $a \bmod c + b \bmod c$, i.e., $(a + b) \bmod c = a \bmod c + b \bmod c$.

Nat.add_mod_add_of_le_add_mod theorem

{a b c : ℕ} (hc : c ≤ a % c + b % c) : (a + b) % c + c = a % c + b % c

Full source

theorem add_mod_add_of_le_add_mod {a b c : ℕ} (hc : c ≤ a % c + b % c) :
    (a + b) % c + c = a % c + b % c := by rw [← add_mod_add_ite, if_pos hc]

Modular Addition Correction When Remainders Sum Exceeds Divisor: $(a + b) \bmod c + c = a \bmod c + b \bmod c$

Informal description

For any natural numbers $a$, $b$, and $c$ such that $c \leq (a \bmod c + b \bmod c)$, the sum of $(a + b) \bmod c$ and $c$ equals $a \bmod c + b \bmod c$, i.e., $$(a + b) \bmod c + c = a \bmod c + b \bmod c.$$

Nat.add_div_eq_of_add_mod_lt theorem

{a b c : ℕ} (hc : a % c + b % c < c) : (a + b) / c = a / c + b / c

Full source

theorem add_div_eq_of_add_mod_lt {a b c : ℕ} (hc : a % c + b % c < c) :
    (a + b) / c = a / c + b / c :=
  if hc0 : c = 0 then by simp [hc0]
  else by rw [Nat.add_div (Nat.pos_of_ne_zero hc0), if_neg (not_le_of_lt hc), add_zero]

Integer Division of Sum When Remainders Sum Below Divisor

Informal description

For any natural numbers $a$, $b$, and $c$ such that $a \bmod c + b \bmod c < c$, the integer division of $a + b$ by $c$ equals the sum of the integer divisions of $a$ by $c$ and $b$ by $c$, i.e., $\lfloor \frac{a + b}{c} \rfloor = \lfloor \frac{a}{c} \rfloor + \lfloor \frac{b}{c} \rfloor$.

Nat.add_div_of_dvd_right theorem

{a b c : ℕ} (hca : c ∣ a) : (a + b) / c = a / c + b / c

Full source

protected theorem add_div_of_dvd_right {a b c : ℕ} (hca : c ∣ a) : (a + b) / c = a / c + b / c :=
  if h : c = 0 then by simp [h]
  else
    add_div_eq_of_add_mod_lt
      (by
        rw [Nat.mod_eq_zero_of_dvd hca, zero_add]
        exact Nat.mod_lt _ (zero_lt_of_ne_zero h))

Integer Division of Sum When Divisor Divides First Term

Informal description

For any natural numbers $a$, $b$, and $c$ such that $c$ divides $a$, the integer division of $a + b$ by $c$ equals the sum of the integer divisions of $a$ by $c$ and $b$ by $c$, i.e., $\lfloor \frac{a + b}{c} \rfloor = \lfloor \frac{a}{c} \rfloor + \lfloor \frac{b}{c} \rfloor$.

Nat.add_div_of_dvd_left theorem

{a b c : ℕ} (hca : c ∣ b) : (a + b) / c = a / c + b / c

Full source

protected theorem add_div_of_dvd_left {a b c : ℕ} (hca : c ∣ b) : (a + b) / c = a / c + b / c := by
  rwa [add_comm, Nat.add_div_of_dvd_right, add_comm]

Integer Division of Sum When Divisor Divides Second Term

Informal description

For any natural numbers $a$, $b$, and $c$ such that $c$ divides $b$, the integer division of $a + b$ by $c$ equals the sum of the integer divisions of $a$ by $c$ and $b$ by $c$, i.e., $\lfloor \frac{a + b}{c} \rfloor = \lfloor \frac{a}{c} \rfloor + \lfloor \frac{b}{c} \rfloor$.

Nat.add_div_eq_of_le_mod_add_mod theorem

{a b c : ℕ} (hc : c ≤ a % c + b % c) (hc0 : 0 < c) : (a + b) / c = a / c + b / c + 1

Full source

theorem add_div_eq_of_le_mod_add_mod {a b c : ℕ} (hc : c ≤ a % c + b % c) (hc0 : 0 < c) :
    (a + b) / c = a / c + b / c + 1 := by rw [Nat.add_div hc0, if_pos hc]

Integer Division Formula When Remainders Sum to at Least Divisor

Informal description

For any natural numbers $a$, $b$, and $c$ such that $c > 0$ and $c \leq a \% c + b \% c$, the integer division of $a + b$ by $c$ satisfies the equality: \[ \frac{a + b}{c} = \frac{a}{c} + \frac{b}{c} + 1 \] where $a \% c$ denotes the remainder of $a$ divided by $c$.

Nat.add_div_le_add_div theorem

(a b c : ℕ) : a / c + b / c ≤ (a + b) / c

Full source

theorem add_div_le_add_div (a b c : ℕ) : a / c + b / c ≤ (a + b) / c :=
  if hc0 : c = 0 then by simp [hc0]
  else by rw [Nat.add_div (Nat.pos_of_ne_zero hc0)]; exact Nat.le_add_right _ _

Subadditivity of Integer Division for Natural Numbers

Informal description

For any natural numbers $a$, $b$, and $c$, the sum of the integer divisions of $a$ by $c$ and $b$ by $c$ is less than or equal to the integer division of $a + b$ by $c$, i.e., \[ \left\lfloor \frac{a}{c} \right\rfloor + \left\lfloor \frac{b}{c} \right\rfloor \leq \left\lfloor \frac{a + b}{c} \right\rfloor. \]

Nat.le_mod_add_mod_of_dvd_add_of_not_dvd theorem

{a b c : ℕ} (h : c ∣ a + b) (ha : ¬c ∣ a) : c ≤ a % c + b % c

Full source

theorem le_mod_add_mod_of_dvd_add_of_not_dvd {a b c : ℕ} (h : c ∣ a + b) (ha : ¬c ∣ a) :
    c ≤ a % c + b % c :=
  by_contradiction fun hc => by
    have : (a + b) % c = a % c + b % c := add_mod_of_add_mod_lt (lt_of_not_ge hc)
    simp_all [dvd_iff_mod_eq_zero]

Lower Bound on Remainder Sum When Divisor Divides Sum but Not First Term

Informal description

For any natural numbers $a$, $b$, and $c$, if $c$ divides $a + b$ but does not divide $a$, then $c$ is less than or equal to the sum of the remainders $a \bmod c$ and $b \bmod c$, i.e., $c \leq a \% c + b \% c$.

Nat.odd_mul_odd theorem

{n m : ℕ} : n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1

Full source

theorem odd_mul_odd {n m : ℕ} : n % 2 = 1 → m % 2 = 1 → n * m % 2 = 1 := by
  simpa [Nat.ModEq] using @ModEq.mul 2 n 1 m 1

Product of Odd Natural Numbers is Odd

Informal description

For any natural numbers $n$ and $m$, if $n$ is odd (i.e., $n \equiv 1 \pmod{2}$) and $m$ is odd (i.e., $m \equiv 1 \pmod{2}$), then their product $n \cdot m$ is also odd (i.e., $n \cdot m \equiv 1 \pmod{2}$).

Nat.odd_mul_odd_div_two theorem

{m n : ℕ} (hm1 : m % 2 = 1) (hn1 : n % 2 = 1) : m * n / 2 = m * (n / 2) + m / 2

Full source

theorem odd_mul_odd_div_two {m n : ℕ} (hm1 : m % 2 = 1) (hn1 : n % 2 = 1) :
    m * n / 2 = m * (n / 2) + m / 2 :=
  have hn0 : 0 < n := Nat.pos_of_ne_zero fun h => by simp_all
  mul_right_injective₀ two_ne_zero <| by
    dsimp
    rw [mul_add, two_mul_odd_div_two hm1, mul_left_comm, two_mul_odd_div_two hn1,
      two_mul_odd_div_two (Nat.odd_mul_odd hm1 hn1), Nat.mul_sub, mul_one, ←
      Nat.add_sub_assoc (by omega), Nat.sub_add_cancel (Nat.le_mul_of_pos_right m hn0)]

Division of Product of Odd Numbers by Two: $\frac{m \cdot n}{2} = m \cdot \left\lfloor \frac{n}{2} \right\rfloor + \left\lfloor \frac{m}{2} \right\rfloor$ for odd $m, n$

Informal description

For any odd natural numbers $m$ and $n$ (i.e., $m \equiv 1 \pmod{2}$ and $n \equiv 1 \pmod{2}$), the integer division of their product by 2 satisfies: \[ \frac{m \cdot n}{2} = m \cdot \left\lfloor \frac{n}{2} \right\rfloor + \left\lfloor \frac{m}{2} \right\rfloor \]

Nat.odd_of_mod_four_eq_one theorem

{n : ℕ} : n % 4 = 1 → n % 2 = 1

Full source

theorem odd_of_mod_four_eq_one {n : ℕ} : n % 4 = 1 → n % 2 = 1 := by
  simpa [ModEq] using @ModEq.of_mul_left 2 n 1 2

Congruence modulo 4 implies congruence modulo 2 for odd numbers

Informal description

For any natural number $n$, if $n \equiv 1 \pmod{4}$, then $n \equiv 1 \pmod{2}$.

Nat.odd_of_mod_four_eq_three theorem

{n : ℕ} : n % 4 = 3 → n % 2 = 1

Full source

theorem odd_of_mod_four_eq_three {n : ℕ} : n % 4 = 3 → n % 2 = 1 := by
  simpa [ModEq] using @ModEq.of_mul_left 2 n 3 2

Congruence modulo 4 implies oddness for remainder 3

Informal description

For any natural number $n$, if $n \equiv 3 \pmod{4}$, then $n \equiv 1 \pmod{2}$.

Nat.odd_mod_four_iff theorem

{n : ℕ} : n % 2 = 1 ↔ n % 4 = 1 ∨ n % 4 = 3

Full source

/-- A natural number is odd iff it has residue `1` or `3` mod `4`. -/
theorem odd_mod_four_iff {n : ℕ} : n % 2 = 1 ↔ n % 4 = 1 ∨ n % 4 = 3 :=
  have help : ∀ m : ℕ, m < 4 → m % 2 = 1 → m = 1 ∨ m = 3 := by decide
  ⟨fun hn =>
    help (n % 4) (mod_lt n (by omega)) <| (mod_mod_of_dvd n (by decide : 2 ∣ 4)).trans hn,
    fun h => Or.elim h odd_of_mod_four_eq_one odd_of_mod_four_eq_three⟩

Characterization of Odd Numbers via Remainders Modulo 4

Informal description

A natural number $n$ is odd if and only if its remainder modulo 4 is either 1 or 3, i.e., $n \equiv 1 \pmod{2} \leftrightarrow (n \equiv 1 \pmod{4} \lor n \equiv 3 \pmod{4})$.

Nat.mod_eq_of_modEq theorem

{a b n} (h : a ≡ b [MOD n]) (hb : b < n) : a % n = b

Full source

lemma mod_eq_of_modEq {a b n} (h : a ≡ b [MOD n]) (hb : b < n) : a % n = b :=
  Eq.trans h (mod_eq_of_lt hb)

Remainder under congruence condition: $a \equiv b \pmod{n}$ and $b < n$ implies $a \% n = b$

Informal description

For any natural numbers $a$, $b$, and $n$, if $a \equiv b \pmod{n}$ and $b < n$, then the remainder of $a$ divided by $n$ is equal to $b$.

Mathlib.Data.Nat.ModEq

Notations

Tags