Nat.odd_of_mod_four_eq_three
theorem Nat.odd_of_mod_four_eq_three : ∀ {n : ℕ}, n % 4 = 3 → n % 2 = 1
This theorem states that for any natural number `n`, if the modulus of `n` divided by 4 equals 3, then the modulus of `n` divided by 2 equals 1. In mathematical terms, it asserts that if `n` modulo 4 is 3, then `n` is necessarily odd (since `n` modulo 2 is 1).
More concisely: If `n` is a natural number with `n` modulo 4 = 3, then `n` is odd, i.e., `n` modulo 2 = 1.
|
Nat.modEq_of_dvd
theorem Nat.modEq_of_dvd : ∀ {n a b : ℕ}, ↑n ∣ ↑b - ↑a → n.ModEq a b
This theorem, `Nat.modEq_of_dvd`, is an alias for the reverse direction of another theorem `Nat.modEq_iff_dvd`. It states that for any natural numbers `n`, `a`, and `b`, if `n` divides the difference between `b` and `a`, then `a` is congruent to `b` modulo `n`. In mathematical terms, this is saying that if `n` is a divisor of `b - a`, then `a ≡ b (mod n)`.
More concisely: If `n` divides `b - a`, then `a` is congruent to `b` modulo `n`.
|
Nat.ModEq.cancel_left_div_gcd
theorem Nat.ModEq.cancel_left_div_gcd : ∀ {m a b c : ℕ}, 0 < m → m.ModEq (c * a) (c * b) → (m / m.gcd c).ModEq a b := by
sorry
This theorem, `Nat.ModEq.cancel_left_div_gcd`, states that for any positive integer modulus `m` and any integers `a`, `b` and `c`, if `c * a` is congruent to `c * b` modulo `m`, then `a` is congruent to `b` modulo `m / gcd(m, c)`. Essentially, this theorem allows us to cancel a common factor `c` from a modular equivalence, but in doing so we must divide the modulus by the greatest common divisor (gcd) of the modulus and `c`.
More concisely: If `a` is congruent to `b` modulo `m`, then `a` is congruent to `b` modulo `m / gcd(m, c)` when `c * a` is congruent to `c * b` modulo `m`.
|
Nat.modEq_zero_iff_dvd
theorem Nat.modEq_zero_iff_dvd : ∀ {n a : ℕ}, n.ModEq a 0 ↔ n ∣ a
The theorem `Nat.modEq_zero_iff_dvd` states that for any two natural numbers `n` and `a`, `a` is congruent to 0 modulo `n` if and only if `n` divides `a`. In mathematical terms, it describes the relation between modulo operation and divisibility: if when `a` is divided by `n` the remainder is 0 (`a ≡ 0 [MOD n]`), then `n` is a divisor of `a` (`n ∣ a`). This theorem makes a direct connection between the concepts of modular arithmetic and divisibility.
More concisely: For any natural numbers `n` and `a`, `a` is congruent to 0 modulo `n` if and only if `n` divides `a`. (Equivalently, `n ∣ a` if and only if `a ≡ 0 [MOD n]`.)
|
Nat.modEq_iff_dvd'
theorem Nat.modEq_iff_dvd' : ∀ {n a b : ℕ}, a ≤ b → (n.ModEq a b ↔ n ∣ b - a)
This theorem states that for any natural numbers `n`, `a`, and `b`, where `a` is less than or equal to `b`, `a` is equivalent to `b` modulo `n` if and only if `n` divides the difference of `b` and `a`. In other words, `a` and `b` have the same remainder when divided by `n` if and only if `b - a` is a multiple of `n`. This is a variant of the theorem `modEq_iff_dvd` with natural number divisibility.
More concisely: For natural numbers `n`, `a`, and `b`, `a` is congruent to `b` modulo `n` if and only if `n` divides the difference `b - a`.
|
Nat.ModEq.add_right_cancel'
theorem Nat.ModEq.add_right_cancel' : ∀ {n a b : ℕ} (c : ℕ), n.ModEq (a + c) (b + c) → n.ModEq a b
The theorem `Nat.ModEq.add_right_cancel'` states that for any natural numbers `n`, `a`, `b`, and `c`, if `a + c` is congruent to `b + c` modulo `n`, then `a` is congruent to `b` modulo `n`. In other words, if two numbers, when added to the same number, give the same remainder when divided by a particular number, then those two original numbers also give the same remainder when divided by that particular number. This is a property of modulo arithmetic.
More concisely: If `a` is congruent to `b` modulo `n` and `c` is any natural number, then `a + c` is congruent to `b + c` modulo `n` implies `a` is congruent to `b` modulo `n`.
|
Nat.ModEq.of_mul_right
theorem Nat.ModEq.of_mul_right : ∀ {n a b : ℕ} (m : ℕ), (n * m).ModEq a b → n.ModEq a b
This theorem, `Nat.ModEq.of_mul_right`, states that for any natural numbers `n`, `a`, `b`, and `m`, if `a` is congruent to `b` modulo `n * m`, then `a` is also congruent to `b` modulo `n`. This is essentially stating that right multiplication can be cancelled out in the modulus. For a theorem that cancels right multiplication on both sides of the congruence relation, refer to `nat.modeq.mul_right_cancel'`.
More concisely: If `a` is congruent to `b` modulo `n * m`, then `a` is congruent to `b` modulo `n`.
|
Nat.ModEq.of_mul_left
theorem Nat.ModEq.of_mul_left : ∀ {n a b : ℕ} (m : ℕ), (m * n).ModEq a b → n.ModEq a b
This theorem, `Nat.ModEq.of_mul_left`, states that for all natural numbers `n`, `a`, `b`, and `m`, if `a` is congruent to `b` modulo `m * n`, then `a` is also congruent to `b` modulo `n`. This allows for cancellation of left-multiplication in modulus calculations. Note that if you need to cancel left multiplication on both sides of the congruence, you should refer to a different theorem, `nat.modeq.mul_left_cancel'`.
More concisely: If `a` is congruent to `b` modulo `m`, then `a` is congruent to `b` modulo `n` for `m = nk`, where `k` is a natural number. (This implies that left cancellation is allowed in modulo arithmetic when the moduli are multiple of a common factor.)
|
Nat.add_mod_add_ite
theorem Nat.add_mod_add_ite : ∀ (a b c : ℕ), ((a + b) % c + if c ≤ a % c + b % c then c else 0) = a % c + b % c := by
sorry
This theorem states that for any three natural numbers a, b, and c, the sum of the modulus of the sum of a and b by c and an additional term - which is c if c is less than or equal to the modulus of the sum of a and b, or 0 otherwise - is equal to the sum of the modulus of a and c and the modulus of b and c. In mathematical terms, this can be written as: `((a + b) mod c) + (c if c ≤ (a mod c + b mod c) else 0) = (a mod c + b mod c)`.
More concisely: For natural numbers a, b, and c, the expression ((a + b) mod c + c if c <= a % c + b % c else 0) equals (a % c + b % c).
|
Nat.ModEq.cancel_right_div_gcd
theorem Nat.ModEq.cancel_right_div_gcd : ∀ {m a b c : ℕ}, 0 < m → m.ModEq (a * c) (b * c) → (m / m.gcd c).ModEq a b
This theorem states that if two natural numbers `a` and `b` are congruent modulo `m`, denoted `m.ModEq`, after each of them has been multiplied by a common factor `c`, then `a` and `b` will also be congruent modulo `m` divided by the greatest common divisor of `m` and `c`, provided `m` is greater than 0. This essentially allows us to cancel the common factor `c` from the `ModEq` by dividing the modulus `m` by `gcd(m, c)`.
More concisely: If `a` is congruent to `b` modulo `m`, and `c` is a common factor of `m` and `a`, then `a` is congruent to `bc^{-1}` modulo `m/gcd(m, c)`, where `gcd` is the greatest common divisor and `c^{-1}` is the multiplicative inverse of `c` modulo `m`.
|
Nat.ModEq.trans
theorem Nat.ModEq.trans : ∀ {n a b c : ℕ}, n.ModEq a b → n.ModEq b c → n.ModEq a c
This theorem, `Nat.ModEq.trans`, demonstrates the transitivity of congruence modulo `n` for natural numbers. In other words, if `a` is congruent to `b` modulo `n`, and `b` is congruent to `c` modulo `n`, then `a` is also congruent to `c` modulo `n`. This transitivity property is a fundamental aspect of modular arithmetic.
More concisely: If `a` is congruent to `b` modulo `n` and `b` is congruent to `c` modulo `n`, then `a` is congruent to `c` modulo `n`. (Modular arithmetic)
|
Nat.ModEq.symm
theorem Nat.ModEq.symm : ∀ {n a b : ℕ}, n.ModEq a b → n.ModEq b a
The theorem `Nat.ModEq.symm` states that for any three natural numbers `n`, `a`, and `b`, if `a` is congruent to `b` modulo `n` (denoted as `a ≡ b [MOD n]`), then `b` is also congruent to `a` modulo `n` (denoted as `b ≡ a [MOD n]`). In other words, the congruence relation modulo `n` is symmetric.
More concisely: If `a` is congruent to `b` modulo `n`, then `b` is congruent to `a` modulo `n` (i.e., `a ≡ b [MOD n]` implies `b ≡ a [MOD n]`).
|
Nat.add_div
theorem Nat.add_div : ∀ {a b c : ℕ}, 0 < c → (a + b) / c = a / c + b / c + if c ≤ a % c + b % c then 1 else 0 := by
sorry
This theorem states that for any natural numbers `a`, `b`, and `c`, given that `c` is greater than 0, the result of dividing the sum of `a` and `b` by `c` is equal to the sum of the results of dividing `a` and `b` by `c` individually, plus an additional 1 if `c` is less than or equal to the sum of the remainders of `a` and `b` when divided by `c`, or plus 0 otherwise. In mathematical terms, `(a + b) / c = a / c + b / c + 1` if `c ≤ a mod c + b mod c`, and `(a + b) / c = a / c + b / c` otherwise.
More concisely: For natural numbers `a`, `b`, and `c` with `c > 0`, `(a + b) / c = a / c + b / c + 1` if `c <= a % c + b % c`, and `(a + b) / c = a / c + b / c` otherwise.
|
Nat.ModEq.cancel_right_of_coprime
theorem Nat.ModEq.cancel_right_of_coprime : ∀ {m a b c : ℕ}, m.gcd c = 1 → m.ModEq (a * c) (b * c) → m.ModEq a b := by
sorry
This theorem states that for any natural numbers `m`, `a`, `b`, and `c`, if `c` is coprime with `m` (i.e., the greatest common divisor of `m` and `c` is 1), and `m` is congruent to `a * c` modulo `b * c`, then `m` is also congruent to `a` modulo `b`. Essentially, it means that a common factor that's coprime with the modulus can be cancelled from a congruence relation.
More concisely: If `m` is congruent to `ac` modulo `bc` and `c` is coprime to `m`, then `m` is congruent to `a` modulo `b`.
|
Nat.ModEq.mul_left_cancel'
theorem Nat.ModEq.mul_left_cancel' : ∀ {a b c m : ℕ}, c ≠ 0 → (c * m).ModEq (c * a) (c * b) → m.ModEq a b
This theorem states that if three natural numbers `a`, `b`, and `c` are given such that `c` is not zero, then if the modulus of `c * m` is equivalent to both `c * a` and `c * b`, it implies that the modulus of `m` is also equivalent to both `a` and `b`. In simpler terms, multiplying a number by a non-zero constant `c` will not change its equivalency when taken modulo `a` and `b`. However, if you want to cancel out the left multiplication in the modulus, refer to the theorem `Nat.ModEq.of_mul_left`.
More concisely: If `c` is a non-zero natural number and `a`, `b`, and `m` are natural numbers such that `c * m` is congruent to both `c * a` and `c * b` modulo some natural number `k`, then `a` is congruent to `b` modulo `k`.
|
Nat.ModEq.mul
theorem Nat.ModEq.mul : ∀ {n a b c d : ℕ}, n.ModEq a b → n.ModEq c d → n.ModEq (a * c) (b * d)
This theorem, `Nat.ModEq.mul`, states that for any natural numbers `n`, `a`, `b`, `c`, `d`, if `a` is equivalent to `b` modulo `n` and `c` is equivalent to `d` modulo `n`, then the product of `a` and `c` is equivalent to the product of `b` and `d` modulo `n`. In mathematical notation, this is saying if a ≡ b (mod n) and c ≡ d (mod n), then a*c ≡ b*d (mod n).
More concisely: If `a` is congruent to `b` and `c` is congruent to `d` modulo `n`, then `ac` is congruent to `bd` modulo `n`.
|
Dvd.dvd.modEq_zero_nat
theorem Dvd.dvd.modEq_zero_nat : ∀ {n a : ℕ}, n ∣ a → n.ModEq a 0
This theorem states that for all natural numbers `n` and `a`, if `n` divides `a` (denoted by `n ∣ a`), then `a` is congruent to 0 modulo `n` (denoted by `a ≡ 0 [MOD n]`). In other words, if `n` is a divisor of `a`, then the remainder of `a` when divided by `n` is 0.
More concisely: If `n` divides `a`, then `a` is congruent to 0 modulo `n`. (In other words, `n` being a divisor of `a` implies `a`'s remainder when divided by `n` is 0.)
|
Nat.ModEq.add
theorem Nat.ModEq.add : ∀ {n a b c d : ℕ}, n.ModEq a b → n.ModEq c d → n.ModEq (a + c) (b + d)
This theorem states that for all natural numbers `n`, `a`, `b`, `c`, and `d`, if `a` is congruent to `b` modulo `n` and `c` is congruent to `d` modulo `n`, then the sum of `a` and `c` is congruent to the sum of `b` and `d` modulo `n`. In other words, congruence modulo `n` is preserved under addition.
More concisely: For all natural numbers `n`, `a`, `b`, `c`, and `d`, if `a ≡ b (mod n)` and `c ≡ d (mod n)`, then `a + c ≡ b + d (mod n)`.
|
Nat.ModEq.mul_left'
theorem Nat.ModEq.mul_left' : ∀ {n a b : ℕ} (c : ℕ), n.ModEq a b → (c * n).ModEq (c * a) (c * b)
This theorem states that for any natural numbers `n`, `a`, `b`, and `c`, if `a` is congruent to `b` modulo `n`, then the product of `c` and `a` is congruent to the product of `c` and `b` modulo `c` times `n`. Essentially, it's showing the property of congruence that allows scaling both sides of the congruence by a constant, while also scaling the modulus by the same constant.
More concisely: For any natural numbers `n`, `a`, `b`, and `c`, if `a ≡ b (mod n)`, then `c * a ≡ c * b (mod n * c)`.
|
Nat.ModEq.mul_left
theorem Nat.ModEq.mul_left : ∀ {n a b : ℕ} (c : ℕ), n.ModEq a b → n.ModEq (c * a) (c * b)
This theorem, `Nat.ModEq.mul_left`, states that for any natural numbers `n`, `a`, `b`, and `c`, if `a` is congruent to `b` modulo `n` (denoted as `a ≡ b [MOD n]`), then the product of `c` and `a` is also congruent to the product of `c` and `b` modulo `n` (denoted as `c * a ≡ c * b [MOD n]`). In other words, if two numbers are congruent modulo `n`, multiplying both by the same value maintains their congruence modulo `n`.
More concisely: If `a` is congruent to `b` modulo `n`, then `c * a` is congruent to `c * b` modulo `n`.
|
Nat.modEq_iff_dvd
theorem Nat.modEq_iff_dvd : ∀ {n a b : ℕ}, n.ModEq a b ↔ ↑n ∣ ↑b - ↑a
This theorem, `Nat.modEq_iff_dvd`, states that for any three natural numbers `n`, `a`, and `b`, `a` is congruent to `b` modulo `n` if and only if `n` divides the difference `b - a`. In other words, if the remainder of `b` when divided by `n` is the same as the remainder of `a` when divided by `n`, then `n` must divide `b - a`. This links the concept of modulo equivalence with the concept of divisibility.
More concisely: For natural numbers n, a, and b, a is congruent to b modulo n if and only if n divides b - a.
|
Nat.odd_mod_four_iff
theorem Nat.odd_mod_four_iff : ∀ {n : ℕ}, n % 2 = 1 ↔ n % 4 = 1 ∨ n % 4 = 3
This theorem states that a natural number is odd if and only if its remainder when divided by 4 is either 1 or 3. In other words, it characterizes odd numbers in terms of their residues modulo 4.
More concisely: A natural number is odd if and only if its residue modulo 4 is 1 or 3.
|
Nat.ModEq.mul_right
theorem Nat.ModEq.mul_right : ∀ {n a b : ℕ} (c : ℕ), n.ModEq a b → n.ModEq (a * c) (b * c)
This theorem, `Nat.ModEq.mul_right`, states that for any natural numbers `n`, `a`, `b`, and `c`, if `a` is congruent to `b` modulo `n` (written as `a ≡ b [MOD n]`), then the product of `a` and `c` is also congruent to the product of `b` and `c` modulo `n` (written as `a * c ≡ b * c [MOD n]`). In other words, if two numbers agree modulo `n`, then their products with any given number also agree modulo `n`.
More concisely: If `a` is congruent to `b` modulo `n`, then `a * c` is congruent to `b * c` modulo `n` for all natural numbers `c`.
|
Nat.ModEq.rfl
theorem Nat.ModEq.rfl : ∀ {n a : ℕ}, n.ModEq a a
This theorem, `Nat.ModEq.rfl`, states that for any two natural numbers `n` and `a`, `a` is congruent to `a` modulo `n`. In other words, when we divide `a` by `n`, the remainder is the same as if we divide `a` by itself. This is a reflexive property inherent to the modulo operation.
More concisely: For all natural numbers n and a, a is congruent to a modulo n. (a ≡ a (mod n)).
|
Nat.ModEq.mul_right_cancel'
theorem Nat.ModEq.mul_right_cancel' : ∀ {a b c m : ℕ}, c ≠ 0 → (m * c).ModEq (a * c) (b * c) → m.ModEq a b
This theorem, `Nat.ModEq.mul_right_cancel'`, states that for all natural numbers `a`, `b`, `c`, and `m`, with `c` not equal to zero, if the modulus of `m * c` and `a * c` is equal to the modulus of `b * c`, then the modulus of `m` is equal to the modulus of `a` and `b`. It essentially allows you to cancel out a common factor on both sides of a modular equation. Note that this theorem is also applicable to cancel right multiplication in the modulus, as per the theorem `Nat.ModEq.of_mul_right`.
More concisely: If `m * c` and `a * c` have the same modulo `m` for some natural numbers `a`, `b`, and non-zero `c`, then `m` equals the modulo of both `a` and `b`.
|
Nat.odd_of_mod_four_eq_one
theorem Nat.odd_of_mod_four_eq_one : ∀ {n : ℕ}, n % 4 = 1 → n % 2 = 1
This theorem states that for any natural number `n`, if the remainder when `n` is divided by 4 equals 1 then the remainder when `n` is divided by 2 also equals 1. In other words, if a natural number is one more than a multiple of 4, then it is an odd number.
More concisely: If a natural number `n` is congruent to 1 modulo 4, then it is congruent to 1 modulo 2.
|
Nat.ModEq.add_right_cancel
theorem Nat.ModEq.add_right_cancel : ∀ {n a b c d : ℕ}, n.ModEq c d → n.ModEq (a + c) (b + d) → n.ModEq a b
This theorem, `Nat.ModEq.add_right_cancel`, states that for any natural numbers `n`, `a`, `b`, `c`, and `d`, if `c` is congruent to `d` modulo `n`, and `a + c` is congruent to `b + d` modulo `n`, then `a` is congruent to `b` modulo `n`. It essentially says that if two numbers add the same amount (`c` or `d`) and the results are congruent modulo `n`, then the original two numbers (`a` and `b`) are also congruent modulo `n`. This theorem proves the property of right cancellation under addition in modular arithmetic.
More concisely: If `a` is congruent to `b` modulo `n`, `c` is congruent to `d` modulo `n`, then `a + c` is congruent to `b + d` modulo `n` implies `a` is congruent to `b` modulo `n`.
|
Nat.ModEq.cancel_left_of_coprime
theorem Nat.ModEq.cancel_left_of_coprime : ∀ {m a b c : ℕ}, m.gcd c = 1 → m.ModEq (c * a) (c * b) → m.ModEq a b := by
sorry
This theorem states that for any non-negative integers `m`, `a`, `b`, and `c`, if the greatest common divisor (gcd) of `m` and `c` is 1 (which means `m` and `c` are coprime), and if `m` is congruent to `c * a` modulo `c * b`, then `m` is also congruent to `a` modulo `b`. In other words, we can cancel a common factor that's coprime with the modulus from a modular equation.
More concisely: If `m` is congruent to `c * a` modulo `c * b` and `gcd(m, c) = 1`, then `m` is congruent to `a` modulo `b`.
|
Nat.modEq_zero_iff
theorem Nat.modEq_zero_iff : ∀ {a b : ℕ}, a ≡ b [MOD 0] ↔ a = b
This theorem establishes a relationship between the modulus operation and equality in natural numbers (ℕ). Specifically, it states that for every pair of natural numbers `a` and `b`, `a` is congruent to `b` modulo 0 if and only if `a` is equal to `b`. In other words, the modulus of `a` divided by `b` is zero only when `a` and `b` are the same number.
More concisely: For all natural numbers `a` and `b`, `a` is congruent to `b` modulo 0 if and only if `a` equals `b`. In other words, `a % b = 0` if and only if `a = b`.
|
Nat.ModEq.dvd
theorem Nat.ModEq.dvd : ∀ {n a b : ℕ}, n.ModEq a b → ↑n ∣ ↑b - ↑a
This theorem is an alias for the forward direction of `Nat.modEq_iff_dvd`. It states that for any natural numbers `n`, `a`, and `b`, if `a` is equivalent to `b` modulo `n` (denoted as `a ≡ b [MOD n]`), then `n` divides the difference between `b` and `a` (expressed as `↑n ∣ ↑b - ↑a`). In mathematical terms, this means if `a` and `b` have the same remainder when divided by `n`, then `n` is a divisor of `b - a`.
More concisely: If `a` is congruent to `b` modulo `n`, then `n` divides the difference between `b` and `a`. In other words, `(a ≡ b [MOD n]) ⟹ ↑n ∣ ↑b - ↑a`.
|
Nat.ModEq.comm
theorem Nat.ModEq.comm : ∀ {n a b : ℕ}, n.ModEq a b ↔ n.ModEq b a
This theorem states that for any three natural numbers `n`, `a`, and `b`, the statement "a is congruent to b modulo n" is equivalent to the statement "b is congruent to a modulo n". In other words, the congruence relation modulo n is symmetric. In mathematical terms, if `a ≡ b [MOD n]` is true, then `b ≡ a [MOD n]` is also true, and vice versa.
More concisely: The congruence relation modulo n is a symmetric equivalence relation.
|
Nat.ModEq.refl
theorem Nat.ModEq.refl : ∀ {n : ℕ} (a : ℕ), n.ModEq a a
This theorem, `Nat.ModEq.refl`, states that for any natural number `a` and any natural number `n`, `a` is congruent to itself modulo `n`. In other words, if you divide `a` and `a` by `n`, the remainders will be the same, which is a property of modulo operation. This is a general truth in number theory and is not dependent on the specific values of `a` or `n`.
More concisely: For all natural numbers `a` and `n`, `a` is congruent to `a` modulo `n`. (Or, more mathematically: For all `a` and `n` in `ℕ`, `a` ≡ a (mod n)).
|
Nat.ModEq.of_dvd
theorem Nat.ModEq.of_dvd : ∀ {m n a b : ℕ}, m ∣ n → n.ModEq a b → m.ModEq a b
This theorem, `Nat.ModEq.of_dvd`, states that for any natural numbers `m`, `n`, `a`, and `b`, if `m` divides `n` and `a` is congruent to `b` modulo `n`, then `a` is also congruent to `b` modulo `m`. In mathematical terms, if $m|n$ and $a ≡ b$ (mod $n$), then $a ≡ b$ (mod $m$). This theorem expresses a property of modular congruence when the modulus is a divisor of another modulus.
More concisely: If `m` divides `n` and `a` is congruent to `b` modulo `n`, then `a` is congruent to `b` modulo `m`. In other words, `m` being a divisor of `n` implies `a % n ≡ b % n` if and only if `a % m ≡ b % m`.
|
Nat.mod_modEq
theorem Nat.mod_modEq : ∀ (a n : ℕ), n.ModEq (a % n) a
This theorem, named `Nat.mod_modEq`, states that for any two natural numbers `a` and `n`, the remainder of `a` divided by `n` (denoted as `a % n`) is congruent to `a` modulo `n` (denoted as `a [MOD n]`). In other words, when `a` is divided by `n`, the remainder is the same whether we consider it in terms of computer science '%' operator or in terms of mathematical modulo operation.
More concisely: For all natural numbers `a` and `n`, `a % n` equals `a mod n`.
|