ZMod.val_mul
theorem ZMod.val_mul : ∀ {n : ℕ} (a b : ZMod n), (a * b).val = a.val * b.val % n
The theorem `ZMod.val_mul` states that for any natural number `n` and any two integers modulo `n`, say `a` and `b`, the value of the product `a * b` modulo `n` (as computed by the `Zmod.val` function), is equivalent to the value of `a` modulo `n` times the value of `b` modulo `n`, all modulo `n`. This theorem essentially expresses the property of congruence in modular arithmetic, showing that multiplication in the ring of integers modulo `n` is well-defined in terms of the equivalence classes of the integers modulo `n`.
More concisely: For any natural number `n` and integers `a` and `b` modulo `n`, `ZMod.val (a * b) = ZMod.val (a % n) * ZMod.val (b % n)` modulo `n`.
|
ZMod.val_le
theorem ZMod.val_le : ∀ {n : ℕ} [inst : NeZero n] (a : ZMod n), a.val ≤ n
The theorem `ZMod.val_le` asserts that for any non-zero natural number `n` and any integer modulo `n` (denoted `a : ZMod n`), the value of `a` (as defined by the function `ZMod.val`) is less than or equal to `n`. This means that in the context of modular arithmetic, the absolute value of an integer modulo `n` or the least natural number in its equivalence class (depending on whether `n` is zero or positive) will always be less than or equal to `n`.
More concisely: For any non-zero natural number `n` and integer `a` congruent to some integer modulo `n` (denoted `a : ZMod n`), the absolute value of `a` is less than or equal to `n`.
|
ZMod.addOrderOf_coe
theorem ZMod.addOrderOf_coe : ∀ (a : ℕ) {n : ℕ}, n ≠ 0 → addOrderOf ↑a = n / n.gcd a
The theorem `ZMod.addOrderOf_coe` states that for any natural number `a` and non-zero natural number `n`, the additive order of the element `a` in the additive monoid of integers modulo `n` (i.e., `ZMod n`) is equal to the quotient of `n` divided by the greatest common divisor of `n` and `a`. The additive order of an element in a monoid is the smallest positive natural number such that adding the element to itself that many times results in the additive identity (in this case, zero representation in `ZMod n`). Note, this theorem is applicable when `ZMod n` is not infinite, that is, `n` is not equal to zero. There's a different version of this theorem, `addOrderOf_coe'`, that is used when `a` is not equal to zero.
More concisely: For any natural number `a` and non-zero natural number `n`, the additive order of `a` in `ZMod n` equals the quotient of `n` and the greatest common divisor of `a` and `n`.
|
ZMod.cast_id
theorem ZMod.cast_id : ∀ (n : ℕ) (i : ZMod n), i.cast = i
The theorem `ZMod.cast_id` asserts that for all natural numbers `n` and all integers modulo `n` denoted by `i`, applying the `ZMod.cast` function to `i` results in `i` itself. In other words, the `ZMod.cast` function acts as the identity function on the integers modulo `n`. This means that casting an integer modulo `n` to another semiring (which is the function of `ZMod.cast`) doesn't change the integer modulo `n` itself.
More concisely: For all natural numbers `n` and integers `i` modulo `n`, `ZMod.cast i = i`.
|
ZMod.val_zero
theorem ZMod.val_zero : ∀ {n : ℕ}, ZMod.val 0 = 0
The theorem `ZMod.val_zero` states that for any natural number `n`, the value of the zero element in the ring of integers modulo `n` is also zero. This holds regardless of the specific value of `n`. In mathematical terms, for ∀ `n ∈ ℕ`, the value of `0` in `Z/nZ` is `0`.
More concisely: For all natural numbers n, the zero element in the ring of integers modulo n is equal to zero.
|
ZMod.val_lt
theorem ZMod.val_lt : ∀ {n : ℕ} [inst : NeZero n] (a : ZMod n), a.val < n
This theorem, `ZMod.val_lt`, states that for every natural number `n` that is not zero, and for any integer `a` modulo `n` (`a : ZMod n`), the value of `a` (`ZMod.val a`) is strictly less than `n`. The value of `a` is defined as the least natural number in its equivalence class in modulo `n` arithmetic. In other words, if you have a non-zero natural number `n` and take any integer modulo `n`, the natural number value of that integer will always be less than `n`.
More concisely: For all natural numbers $n \neq 0$ and integers $a$ modulo $n$, the value of $a$ in modulo $n$ arithmetic is strictly less than $n$. Or, in Lean notation, `(∀ (n : ℕ) (a : ZMod n) (h : 0 < n), n < ZMod.val a)`.
|
ZMod.val_eq_zero
theorem ZMod.val_eq_zero : ∀ {n : ℕ} (a : ZMod n), a.val = 0 ↔ a = 0
The theorem `ZMod.val_eq_zero` states that for any natural number `n` and an element `a` of the integers modulo `n` (`ZMod n`), the value function `ZMod.val a` equals to zero if and only if `a` equals to zero. In other words, in the set of integers modulo `n`, the value of an element is zero if and only if the element itself is zero.
More concisely: For all natural numbers n and elements a in ZMod n (integers modulo n), ZMod.val a = 0 if and only if a = 0.
|
ZMod.addOrderOf_coe'
theorem ZMod.addOrderOf_coe' : ∀ {a : ℕ} (n : ℕ), a ≠ 0 → addOrderOf ↑a = n / n.gcd a
This theorem asserts that for any natural numbers `a` and `n`, where `a` is not equal to zero, the additive order of the element `a` (coerced to an integer) is equal to `n` divided by the greatest common divisor of `n` and `a`. The additive order of an element `a` in this context is the smallest natural number `n` such that `n * a = 0`, if such a number exists. If no such natural number exists (if `a` is of infinite order), the additive order is defined to be zero. Note that this theorem applies particularly in cases where the set of integers modulo `n` (denoted as `ZMod n` in Lean) is not infinite, that is, `n` is not equal to zero.
More concisely: For any natural number `n` and non-zero integer `a`, the additive order of `a` modulo `n` is equal to `n` divided by the greatest common divisor of `a` and `n`.
|
RingHom.ext_zmod
theorem RingHom.ext_zmod : ∀ {n : ℕ} {R : Type u_1} [inst : Semiring R] (f g : ZMod n →+* R), f = g
This theorem, named `RingHom.ext_zmod`, states that for any natural number `n` and any type `R` that has a semiring structure, if `f` and `g` are two ring homomorphisms from the integers modulo `n` to `R`, then `f` and `g` must be the same. In other words, any two ring homomorphisms from the integers modulo `n` to a semiring are identical. This is a property about the uniqueness of ring homomorphisms between these two structures.
More concisely: For any natural number `n` and any semiring `R`, any two ring homomorphisms from the integers modulo `n` to `R` are equal.
|
ZMod.prime_ne_zero
theorem ZMod.prime_ne_zero : ∀ (p q : ℕ) [hp : Fact p.Prime] [hq : Fact q.Prime], p ≠ q → ↑q ≠ 0
The theorem `ZMod.prime_ne_zero` states that for any two natural numbers `p` and `q`, if `p` and `q` are both prime numbers, then if `p` is not equal to `q`, the modular inverse of `q` is not zero. In other words, if two natural numbers are distinct primes, then the modular inverse of one cannot be zero.
More concisely: If two natural numbers `p` and `q` are distinct prime numbers, then there is no modular inverse `x` such that `q` mod `p` = `x` \* `p`.
|
ZMod.valMinAbs_def_pos
theorem ZMod.valMinAbs_def_pos :
∀ {n : ℕ} [inst : NeZero n] (x : ZMod n), x.valMinAbs = if x.val ≤ n / 2 then ↑x.val else ↑x.val - ↑n
This theorem, `ZMod.valMinAbs_def_pos`, establishes the definition of the `valMinAbs` function for positive natural numbers `n` and any integer modulo `n`, denoted as `x : ZMod n`. The function `valMinAbs` returns the integer that is in the same equivalence class as `x` and is closest to `0`, with the result being in the interval `(-n/2, n/2]`. The theorem states that the value of `valMinAbs x` is equal to `x` if `x` is less than or equal to `n/2`, otherwise it's equal to `x - n`.
More concisely: For any natural number `n` and integer `x` in `ZMod n`, `valMinAbs x = x` if `x ≤ n / 2`, otherwise `valMinAbs x = x - n`.
|
ZMod.coe_valMinAbs
theorem ZMod.coe_valMinAbs : ∀ {n : ℕ} (x : ZMod n), ↑x.valMinAbs = x
This theorem states that for any natural number `n` and any integer modulo `n` (represented by `x : ZMod n`), the coercion of the integer that is closest to `0` in the same equivalence class as `x` (which is represented by `ZMod.valMinAbs x`) equals `x` itself. In other words, `x` is equal to its own minimum absolute value in its equivalence class when modded by `n`, following the appropriate coercion.
More concisely: For any natural number `n` and integer `x` modulo `n` (represented by `x : ZMod n`), `ZMod.valMinAbs x = x`.
|
ZMod.cast_neg_one
theorem ZMod.cast_neg_one : ∀ {R : Type u_1} [inst : Ring R] (n : ℕ), (-1).cast = ↑n - 1
The theorem `ZMod.cast_neg_one` states that for any ring `R` and natural number `n`, the casting of `-1` in the modular arithmetic system `ZMod n` is equivalent to `n - 1` in `R`. This allows us to avoid the characteristic assumption typically required in `cast_neg`.
More concisely: For any ring R and natural number n, the casting of -1 in ZMod n equals n - 1 in R.
|
ZMod.eq_iff_modEq_nat
theorem ZMod.eq_iff_modEq_nat : ∀ (n : ℕ) {a b : ℕ}, ↑a = ↑b ↔ n.ModEq a b
This theorem states that for any natural number `n`, and any two natural numbers `a` and `b`, the integer forms of `a` and `b` are equal if and only if `a` is congruent to `b` modulo `n`. In other words, `a` and `b` have the same remainder when divided by `n`. The theorem connects modular arithmetic to integer equality.
More concisely: For any natural numbers `n`, `a`, and `b`, `a` and `b` have the same integer value modulo `n` if and only if `a` is equal to `b` as integers.
|
ZMod.val_add
theorem ZMod.val_add : ∀ {n : ℕ} [inst : NeZero n] (a b : ZMod n), (a + b).val = (a.val + b.val) % n
This theorem, `ZMod.val_add`, states that for every natural number `n` that is not zero, and for any two integers `a` and `b` modulo `n` (`ZMod n`), the value (`ZMod.val`) of the sum of `a` and `b` is equal to the remainder of the sum of the values of `a` and `b` when divided by `n`. In mathematical notation, it can be represented as: for all `n ≠ 0`, `a`, `b` in `ZMod n`, we have `val(a + b) = (val(a) + val(b)) mod n`. This theorem essentially states a property of modular arithmetic where the value of the sum of two numbers modulo `n` can be computed by adding the numbers first and then taking the modulus.
More concisely: For all natural numbers `n` not equal to zero and integers `a`, `b` in `ZMod n`, the sum `a + b` in `ZMod n` equals the remainder of `(val(a) + val(b))` when divided by `n`.
|
ZMod.natAbs_valMinAbs_le
theorem ZMod.natAbs_valMinAbs_le : ∀ {n : ℕ} [inst : NeZero n] (x : ZMod n), x.valMinAbs.natAbs ≤ n / 2
This theorem states that for any non-zero natural number `n` and any element `x` from the integers modulo `n`, the absolute value of the minimum absolute value representation of `x` is less than or equal to `n / 2`. In other words, the absolute value of the integer within the same equivalence class as `x` (from the integers modulo `n`) that is closest to `0` is always less than or equal to `n/2`. This ensures that the representative chosen for each equivalence class in modulo `n` arithmetic is as close as possible to zero.
More concisely: For any non-zero integer `x` modulo `n`, the absolute value of its minimum representative is bounded by `n/2`.
|
ZMod.val_coe_unit_coprime
theorem ZMod.val_coe_unit_coprime : ∀ {n : ℕ} (u : (ZMod n)ˣ), (↑u).val.Coprime n
This theorem states that for any natural number `n` and any unit `u` from the group of units of integers modulo `n` (denoted as `(ZMod n)ˣ`), the value of `u` (obtained using the `ZMod.val` function and then coercing `u` to integer) is coprime with `n`. In other words, the greatest common divisor (gcd) of `ZMod.val ↑u` and `n` is 1, meaning that they share no common factor other than 1.
More concisely: For any natural number `n` and unit `u` in `(ZMod n)ˣ`, the greatest common divisor of `n` and the integer representation of `u` is 1.
|
ZMod.ringChar_zmod_n
theorem ZMod.ringChar_zmod_n : ∀ (n : ℕ), ringChar (ZMod n) = n
This theorem states that for all natural numbers `n`, the unique characteristic of the semiring `ZMod n` (the integers modulo `n`) is equal to `n` itself. In other words, it says that the characteristic of the ring of integers modulo `n` is `n`.
More concisely: The characteristic of the ring of integers modulo n is equal to n for all natural numbers n.
|
Mathlib.Data.ZMod.Basic._auxLemma.7
theorem Mathlib.Data.ZMod.Basic._auxLemma.7 : ∀ {m n k : ℕ}, (m.lcm n ∣ k) = (m ∣ k ∧ n ∣ k)
The theorem `Mathlib.Data.ZMod.Basic._auxLemma.7` states that for all natural numbers `m`, `n`, and `k`, the least common multiple (lcm) of `m` and `n` divides `k` if and only if both `m` and `n` divide `k`. In other words, the lcm of two numbers `m` and `n` is a divisor of a number `k` precisely when both `m` and `n` are divisors of `k`.
More concisely: The least common multiple of natural numbers $m$ and $n$ is a divisor of a natural number $k$ if and only if both $m$ and $n$ are divisors of $k$.
|