ZMod.ne_zero_of_gcd_eq_one
theorem ZMod.ne_zero_of_gcd_eq_one : ∀ {a : ℤ} {p : ℕ}, p.Prime → a.gcd ↑p = 1 → ↑a ≠ 0
This theorem states that for any integer `a` and a prime number `p`, if the greatest common divisor (GCD) of `a` and `p` is 1, then the value of `a` in the modulo `p` system is not zero. In other words, if `a` and `p` are coprime (their GCD is 1), then `a` does not become zero when we reduce it modulo `p`.
More concisely: If integers `a` and `p` are coprime (i.e., their greatest common divisor is 1), then `a` is not congruent to zero modulo `p`.
|
ZMod.eq_zero_iff_gcd_ne_one
theorem ZMod.eq_zero_iff_gcd_ne_one : ∀ {a : ℤ} {p : ℕ} [pp : Fact p.Prime], ↑a = 0 ↔ a.gcd ↑p ≠ 1
The theorem `ZMod.eq_zero_iff_gcd_ne_one` states that: for any integer `a` and any prime number `p`, the integer `a` modulo `p` (represented as `a : ZMod p`) is zero if and only if the greatest common divisor of `a` and `p` is not equal to 1. In other words, if `a` is divisible by `p` (i.e., `a mod p = 0`), then `a` and `p` share some common factor other than 1; conversely, if `a` and `p` share some common factor other than 1, then `a` is divisible by `p`. This theorem is a statement about the relationship between modular arithmetic and integer divisibility in the context of prime numbers.
More concisely: For any integer `a` and prime number `p`, `a % p = 0` if and only if `gcd(a, p) ≠ 1`.
|
ZMod.eq_zero_of_gcd_ne_one
theorem ZMod.eq_zero_of_gcd_ne_one : ∀ {a : ℤ} {p : ℕ}, p.Prime → a.gcd ↑p ≠ 1 → ↑a = 0
This theorem states that if we have an integer `a` and a prime number `p` such that the greatest common divisor (gcd) of `a` and `p` is not equal to `1`, then the residue of `a` modulo `p` is zero. In other words, if `a` and `p` share a common factor other than `1`, then `a` is divisible by `p`.
More concisely: If the greatest common divisor of integers `a` and `p` is not `1`, then `a` is congruent to zero modulo `p`. (Or, equivalently, `p` divides `a`.)
|