Int.ModEq.of_mul_left
theorem Int.ModEq.of_mul_left : ∀ {n a b : ℤ} (m : ℤ), (m * n).ModEq a b → n.ModEq a b
This theorem states that for all integer numbers `n`, `a`, `b`, and `m`, if `a` is congruent to `b` modulo `m*n` (written as `a ≡ b [ZMOD m * n]`), then `a` is also congruent to `b` modulo `n` (written as `a ≡ b [ZMOD n]`). The congruence modulo is a relation that says that the numbers leave the same remainder when divided by the modulus.
More concisely: If `a` is congruent to `b` modulo `m*n`, then `a` is congruent to `b` modulo `n`. In other words, `(a ≡ b [ZMOD m * n])` implies `(a ≡ b [ZMOD n])` in the integers modulo `zmod`.
|
Int.ModEq.add
theorem Int.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 any integers `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 `a + c` is also congruent to the sum `b + d` modulo `n`. In other words, the congruence of integers modulo a certain number is preserved under addition.
More concisely: If `a` is congruent to `b` (modulo `n`) and `c` is congruent to `d` (modulo `n`), then `a + c` is congruent to `b + d` (modulo `n`).
|
Mathlib.Data.Int.ModEq._auxLemma.2
theorem Mathlib.Data.Int.ModEq._auxLemma.2 : ∀ {m n k : ℤ}, (m % n = k % n) = ((m - k) % n = 0)
This is a theorem about modular arithmetic for integers. It states that for any three integers `m`, `n`, and `k`, `m` is congruent to `k` modulo `n` (that is, `m` and `k` have the same remainder when divided by `n`) if and only if the difference `m - k` is divisible by `n` (that is, `m - k` modulo `n` is zero). This theorem is a key result in number theory and serves as a fundamental concept in modular arithmetic.
More concisely: For integers m, n, and k, m is congruent to k modulo n if and only if m - k is divisible by n.
|
Int.ModEq.cancel_left_div_gcd
theorem Int.ModEq.cancel_left_div_gcd : ∀ {m a b c : ℤ}, 0 < m → m.ModEq (c * a) (c * b) → (m / ↑(m.gcd c)).ModEq a b
This theorem states that to cancel a common factor `c` from a modular equation, we must divide the modulus `m` by `gcd(m, c)`. In other words, if `m`, `a`, `b`, and `c` are integers, and `m` is greater than 0, then if `m` is congruent modulo to the multiplication of `c` and `a`, and the multiplication of `c` and `b`, it follows that `m` divided by the greatest common divisor of `m` and `c` is congruent modulo to `a` and `b`.
More concisely: If integers `m`, `a`, `b`, and `c` satisfy `m ≡ ac (mod m)` and `gcd(m, c) = d`, then `m / d ≡ a (mod b)`.
|
Mathlib.Data.Int.ModEq._auxLemma.3
theorem Mathlib.Data.Int.ModEq._auxLemma.3 : ∀ (a b : ℤ), (a ∣ b) = (b % a = 0)
This theorem states that for any two integers `a` and `b`, `a` divides `b` if and only if the remainder of the division of `b` by `a` is zero. In other words, if `b` divided by `a` leaves no remainder (i.e., `b % a = 0`), then `a` is a factor of `b`. Conversely, if `a` is a factor of `b`, then `b` divided by `a` will leave no remainder.
More concisely: For integers `a` and `b`, `a` divides `b` if and only if the remainder of `b` divided by `a` is zero.
|
Int.mod_modEq
theorem Int.mod_modEq : ∀ (a n : ℤ), n.ModEq (a % n) a
This theorem, `Int.mod_modEq`, states that for any two integers `a` and `n`, the remainder of `a` divided by `n` is congruent to `a` modulo `n`. In mathematical notation, it means that `a % n` is equivalent to `a [ZMOD n]`. This asserts the basic property of modulo operation in the field of integer numbers.
More concisely: For any integers `a` and `n`, `a % n` is equivalent to `a` modulo `n` in the sense of congruences.
|
Int.ModEq.symm
theorem Int.ModEq.symm : ∀ {n a b : ℤ}, n.ModEq a b → n.ModEq b a
This theorem, `Int.ModEq.symm`, states that for all integers `n`, `a`, and `b`, if `a` is congruent to `b` modulo `n`, then `b` is also congruent to `a` modulo `n`. In mathematical terms, if `a ≡ b (mod n)`, then `b ≡ a (mod n)`. This is the symmetry property of congruence mod `n`.
More concisely: For all integers `n`, `a`, and `b`, 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)`).
|
Int.ModEq.cancel_right_div_gcd
theorem Int.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 given four integers `m`, `a`, `b`, and `c`, with `m` being positive, if `m` is congruent to `a * c` modulo `b * c`, then `m` divided by the greatest common divisor of `m` and `c` is congruent to `a` modulo `b`. This essentially means that we can cancel a common factor `c` from a modulus equation, but in doing so, we need to divide the modulus `m` by the greatest common divisor of `m` and `c`.
More concisely: If `m` is congruent to `a * c` modulo `b * c`, then `m / gcd(m, c)` is congruent to `a` modulo `b`.
|
Int.ModEq.dvd
theorem Int.ModEq.dvd : ∀ {n a b : ℤ}, n.ModEq a b → n ∣ b - a
The theorem `Int.ModEq.dvd` is an alias of the forward direction of another theorem `Int.modEq_iff_dvd`. It states that for any integers `n`, `a`, and `b`, if `a` is congruent to `b` modulo `n` (denoted as `a ≡ b [ZMOD n]`), then `n` divides the difference between `b` and `a` (denoted as `n ∣ b - a`). In other words, if the remainder of `a` divided by `n` equals the remainder of `b` divided by `n`, then `n` is a divisor of the difference `b - a`.
More concisely: If `a` is congruent to `b` modulo `n`, then `n` divides the difference between `a` and `b`.
|
Int.ModEq.add_left_cancel
theorem Int.ModEq.add_left_cancel : ∀ {n a b c d : ℤ}, n.ModEq a b → n.ModEq (a + c) (b + d) → n.ModEq c d
This theorem, `Int.ModEq.add_left_cancel`, states that for any integers `n`, `a`, `b`, `c`, and `d`, if `a` is congruent to `b` modulo `n` and `a + c` is congruent to `b + d` modulo `n`, then `c` is congruent to `d` modulo `n`. In other words, it establishes that in the context of integer modular arithmetic, adding the same value to both sides of a congruence equation allows for cancellation on the left side.
More concisely: If `a` is congruent to `b` modulo `n` and `a + c` is congruent to `b + d` modulo `n`, then `c` is congruent to `d` modulo `n`. (In other words, if `a ≡ b (mod n)` and `a + c ≡ b + d (mod n)`, then `c ≡ d (mod n)` in the context of integer modular arithmetic.)
|
Int.ModEq.rfl
theorem Int.ModEq.rfl : ∀ {n a : ℤ}, n.ModEq a a
This theorem states that for all integers `n` and `a`, `a` is congruent to `a` modulo `n`. In mathematical terms, this means that the remainder of the division of `a` by `n` is the same as the remainder of the division of `a` by `n`, which is always true.
More concisely: For all integers `n` and `a`, `a` is congruent to `a` modulo `n`. (In other words, `a` `≡` `a` (mod `n`) always holds.)
|
Int.ModEq.refl
theorem Int.ModEq.refl : ∀ {n : ℤ} (a : ℤ), n.ModEq a a
This theorem, `Int.ModEq.refl`, states that for any integer `n` and any integer `a`, `a` is congruent to itself modulo `n`. In more mathematical terms, for all integers `a` and `n`, it holds that `a` ≡ `a` (mod `n`), which means that the remainder of dividing `a` by `n` is the same as the remainder of dividing `a` by `n`. This is essentially an assertion of the reflexivity of congruence modulo `n`, a basic property in number theory.
More concisely: For all integers `n` and `a`, `a` is congruent to `a` modulo `n`. (i.e., `a` ≡ `a` (mod `n`)) or equivalently, the remainder of `a` divided by `n` is equal to the remainder of `a` divided by `n` (i.e., `a % n = a % n`).
|
Int.modEq_zero_iff_dvd
theorem Int.modEq_zero_iff_dvd : ∀ {n a : ℤ}, n.ModEq a 0 ↔ n ∣ a
This theorem states that for any two integers `n` and `a`, `a` is congruent to `0` modulo `n` if and only if `n` divides `a`. In other words, if there's an integer `k` so that `n * k = a`, then the remainder of `a` divided by `n` is `0`, and vice versa. This is a fundamental property in number theory that establishes a direct link between the divisibility of two integers and their congruence relation in modular arithmetic.
More concisely: A natural number `n` divides an integer `a` if and only if `a` is congruent to `0` modulo `n`.
|
Int.modEq_iff_dvd
theorem Int.modEq_iff_dvd : ∀ {n a b : ℤ}, n.ModEq a b ↔ n ∣ b - a
This theorem states that for any three integers `n`, `a`, and `b`, `a` is congruent to `b` modulo `n` if and only if `n` divides the difference of `b` and `a`. The left-hand side represents a congruence relationship in modulo arithmetic, where `a` and `b` leave the same remainder when divided by `n`. The right-hand side signifies a divisibility relationship, where `n` divides evenly into the difference between `b` and `a`. Thus, the theorem connects these two mathematical concepts, showing that they are equivalent under these conditions.
More concisely: For integers `n`, `a`, and `b`, `a` is congruent to `b` modulo `n` if and only if `n` divides `b - a`.
|
Int.modEq_add_fac
theorem Int.modEq_add_fac : ∀ {a b n : ℤ} (c : ℤ), n.ModEq a b → n.ModEq (a + n * c) b
This theorem, `Int.modEq_add_fac`, states that for any integers `a`, `b`, `n` and `c`, if `a` is congruent to `b` modulo `n`, then the expression `a + n * c` is also congruent to `b` modulo `n`. In other words, adding any multiple of `n` to `a` doesn't change its congruence class modulo `n`, if `a` is already congruent to `b` modulo `n`. This is a fundamental property of modular arithmetic.
More concisely: If `a` is congruent to `b` modulo `n`, then `a + n*c` is congruent to `b + n*c` modulo `n` for any integer `c`.
|
Int.modEq_of_dvd
theorem Int.modEq_of_dvd : ∀ {n a b : ℤ}, n ∣ b - a → n.ModEq a b
This theorem, `Int.modEq_of_dvd`, is an alias for the reverse direction of `Int.modEq_iff_dvd`. It states that for any three integers `n`, `a` and `b`, if `n` divides the difference `b - a`, then `a` is equivalent to `b` modulo `n`. In other words, the remainder when `b` is divided by `n` is equal to `a`.
More concisely: If `n` divides `b - a`, then `a` is congruent to `b` modulo `n`.
|