ZMod.sum_mul_div_add_sum_mul_div_eq_mul
theorem ZMod.sum_mul_div_add_sum_mul_div_eq_mul :
∀ (p q : ℕ) [hp : Fact p.Prime],
↑q ≠ 0 →
(((Finset.Ico 1 (p / 2).succ).sum fun a => a * q / p) + (Finset.Ico 1 (q / 2).succ).sum fun a => a * p / q) =
p / 2 * (q / 2)
This theorem states that for any two natural numbers `p` and `q`, where `p` is a prime number and `q` is not zero, the sum of each element `a` in set `1` to `p/2` (inclusive of `1` and exclusive of `p/2`) multiplied by `q` and divided by `p`, plus the sum of each element `a` in set `1` to `q/2` (inclusive of `1` and exclusive of `q/2`) multiplied by `p` and divided by `q`, is equal to the product of `p/2` and `q/2`. Essentially, this is a geometrical interpretation of the sum of fractions where the sums represent the number of integer points in each of the two triangles formed by the diagonal of the rectangle with dimensions `(0, p/2) × (0, q/2)`, and the product represents the total number of points in the rectangle.
More concisely: For any prime number `p` and non-zero natural number `q`, the sum of `(a �odiv p) * q` for `a` in the range `1` to `p/2`, and the sum of `(b �odiv q) * p` for `b` in the range `1` to `q/2`, are equal to `(p/2) * (q/2)`.
|
ZMod.gauss_lemma
theorem ZMod.gauss_lemma :
∀ {p : ℕ} [h : Fact p.Prime] {a : ℤ},
p ≠ 2 →
↑a ≠ 0 →
legendreSym p a = (-1) ^ (Finset.filter (fun x => p / 2 < (↑a * ↑x).val) (Finset.Ico 1 (p / 2).succ)).card
**Gauss' Lemma**: This theorem states that for any prime number `p` (not equal to 2) and any integer `a` (not equal to 0), the Legendre symbol of `a` and `p` can be computed by considering the number of natural numbers less than `p/2` for which the value of `(a * x) % p` is greater than `p / 2`. The Legendre symbol is equal to `(-1)` raised to the power of the count of such numbers. The Legendre symbol essentially tells whether `a` is a quadratic residue modulo `p`. Gauss' Lemma offers a way to compute this symbol by considering a certain set of natural numbers.
More concisely: The Legendre symbol of integer `a` modulo prime `p` is equal to `(-1)` raised to the power of the number of integers `x` less than `p/2` such that `(a * x) % p` is strictly greater than `p/2`.
|
ZMod.eisenstein_lemma
theorem ZMod.eisenstein_lemma :
∀ {p : ℕ} [inst : Fact p.Prime],
p ≠ 2 →
∀ {a : ℕ}, a % 2 = 1 → ↑a ≠ 0 → legendreSym p ↑a = (-1) ^ (Finset.Ico 1 (p / 2).succ).sum fun x => x * a / p
**Eisenstein's Lemma**: For any prime number `p` that is not equal to `2`, and for any natural number `a` such that `a` is odd and not equal to `0`, the Legendre symbol of `p` and `a` equals `(-1)` raised to the power of the sum of the terms in the interval from `1` to `p / 2 + 1`, where each term is the product of `x` and `a` divided by `p`. Here, the Legendre symbol is `0` if `a` is `0` modulo `p`, `1` if `a` is a non-zero square modulo `p`, and `-1` otherwise.
More concisely: For prime number `p` not equal to 2 and odd natural number `a`, the Legendre symbol is equal to `(−1) ^ ∑ₙ (x ^ n * a / p)` for `1 ≤ n ≤ p / 2 + 1`, where `x` is a primitive root modulo `p`.
|
ZMod.Ico_map_valMinAbs_natAbs_eq_Ico_map_id
theorem ZMod.Ico_map_valMinAbs_natAbs_eq_Ico_map_id :
∀ (p : ℕ) [hp : Fact p.Prime] (a : ZMod p),
a ≠ 0 →
Multiset.map (fun x => (a * ↑x).valMinAbs.natAbs) (Finset.Ico 1 (p / 2).succ).val =
Multiset.map (fun a => a) (Finset.Ico 1 (p / 2).succ).val
This theorem states that for any prime number `p` and any nonzero integer `a` modulo `p`, the multiset obtained by mapping each nonzero natural number `x` less than or equal to `p / 2` to the absolute value of the integer in `(-p/2, p/2]` that is congruent to `a * x mod p`, is the same as the multiset obtained by keeping the natural numbers `x` unchanged. In other words, the multiset of absolute values of residues modulo `p` (after multiplication with `a`) is the same as the multiset of original numbers under the condition that the numbers considered are in the interval `[1, p/2]`.
More concisely: For any prime number p and nonzero integer a modulo p, the multiset of absolute values of residues a * x modulo p for x in [1, p/2] is equal to the multiset of x in [1, p/2].
|