ZMod.exists_sq_eq_two_iff
theorem ZMod.exists_sq_eq_two_iff : ∀ {p : ℕ} [inst : Fact p.Prime], p ≠ 2 → (IsSquare 2 ↔ p % 8 = 1 ∨ p % 8 = 7) := by
sorry
The theorem `ZMod.exists_sq_eq_two_iff` states that for any natural number `p` that is prime (excluding `2`), `2` is a square modulo `p` if and only if `p` is congruent to either `1` or `7` modulo `8`. In other words, if you have an odd prime number `p`, 2 will have a square root modulo `p` exactly when `p` leaves a remainder of `1` or `7` when divided by `8`.
More concisely: For an odd prime number `p`, `2` is a square modulo `p` if and only if `p` is congruent to `1` or `7` modulo `8`.
|
ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one
theorem ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one :
∀ {p q : ℕ} [inst : Fact p.Prime] [inst_1 : Fact q.Prime], p % 4 = 1 → q ≠ 2 → (IsSquare ↑q ↔ IsSquare ↑p) := by
sorry
The theorem `ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one` states that for all natural numbers `p` and `q` that are odd primes (i.e., both `p` and `q` are prime numbers and `q` is not 2), if `p` is congruent to 1 modulo 4 (i.e., the remainder when `p` is divided by 4 is 1), then `q` is a square modulo `p` if and only if `p` is a square modulo `q`. In other words, `q` has a square root under the modulus `p` if and only if `p` has a square root under the modulus `q`. This is a result in number theory related to the reciprocity law of quadratic residues.
More concisely: For odd primes p and q with p congruent to 1 modulo 4, p has a square root modulo q if and only if q has a square root modulo p.
|
legendreSym.quadratic_reciprocity
theorem legendreSym.quadratic_reciprocity :
∀ {p q : ℕ} [inst : Fact p.Prime] [inst_1 : Fact q.Prime],
p ≠ 2 → q ≠ 2 → p ≠ q → legendreSym q ↑p * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2))
The theorem, known as "The Law of Quadratic Reciprocity," states that for any two distinct odd prime numbers `p` and `q`, the product of the Legendre symbol of `p` with respect to `q` and the Legendre symbol of `q` with respect to `p` equals `(-1)` to the power of `((p-1)*(q-1))/4`. This theorem is a fundamental result in number theory, specifically in the area of quadratic residues. The Legendre symbol is a mathematical function that outputs `0`, `1`, or `-1` based on whether its input is `0` modulo the prime, a nonzero square modulo the prime, or otherwise, respectively.
More concisely: For any distinct odd primes p and q, the Legendre symbols of p with respect to q and q with respect to p are equal to (-1)^{(p-1)(q-1)/4}.
|
ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_three
theorem ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_three :
∀ {p q : ℕ} [inst : Fact p.Prime] [inst_1 : Fact q.Prime],
p % 4 = 3 → q % 4 = 3 → p ≠ q → (IsSquare ↑q ↔ ¬IsSquare ↑p)
This theorem states that, for any two distinct prime numbers `p` and `q` that are both congruent to `3` modulo `4`, `q` is a square (i.e., there exists an integer `r` such that `q = r * r`) modulo `p` if and only if `p` is not a square modulo `q`. This is a statement about the properties of squares and prime numbers in modular arithmetic.
More concisely: For distinct primes p and q congruent to 3 modulo 4, q is a square modulo p if and only if p is not a square modulo q.
|
legendreSym.quadratic_reciprocity'
theorem legendreSym.quadratic_reciprocity' :
∀ {p q : ℕ} [inst : Fact p.Prime] [inst_1 : Fact q.Prime],
p ≠ 2 → q ≠ 2 → legendreSym q ↑p = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q
The theorem `legendreSym.quadratic_reciprocity'` states the Law of Quadratic Reciprocity. According to this theorem, for any two odd prime numbers `p` and `q`, the Legendre symbol of `p` with respect to `q` equals `(-1) ^ ((p-1)(q-1)/4)` times the Legendre symbol of `q` with respect to `p`. This means that the Legendre symbol, which indicates the residual properties of squares in modular arithmetic, shows a certain symmetry between pairs of odd primes. Please note that this theorem specifically excludes the prime number 2.
More concisely: For odd primes p and q, the Legendre symbols of p and q with respect to each other are related by the equation: `(QuadraticChar p q) = (-1) ^ ((p-1)(q-1)/4) * (QuadraticChar q p)`, where `QuadraticChar` denotes the Legendre symbol.
|
legendreSym.at_two
theorem legendreSym.at_two : ∀ {p : ℕ} [inst : Fact p.Prime], p ≠ 2 → legendreSym p 2 = ZMod.χ₈ ↑p
The theorem `legendreSym.at_two` asserts that for any prime number `p` that is not equal to 2, the value of the Legendre symbol of `p` and `2` is given by the first primitive quadratic character on `ZMod 8` evaluated at `p`. The Legendre symbol is a function used in number theory which encodes information about whether a number is a quadratic residue modulo a prime, while the first primitive quadratic character on `ZMod 8` is related to the number field extension $\mathbb{Q}(\sqrt{2})/\mathbb{Q}$.
More concisely: For any odd prime number `p`, the Legendre symbol of `p` and `2` equals the value of the first primitive quadratic character on `ZMod 8` at `p`.
|
ZMod.exists_sq_eq_neg_two_iff
theorem ZMod.exists_sq_eq_neg_two_iff :
∀ {p : ℕ} [inst : Fact p.Prime], p ≠ 2 → (IsSquare (-2) ↔ p % 8 = 1 ∨ p % 8 = 3)
The theorem states that for any natural number `p` which is prime and is not equal to `2`, `-2` is a square number in modulo `p` if and only if `p` is congruent to `1` or `3` modulo `8`. In simpler terms, `-2` is a square number under modulo arithmetic with an odd prime number `p` if, and only if, `p` divided by `8` leaves a remainder of `1` or `3`.
More concisely: For an odd prime number `p`, `-2` is a square number modulo `p` if and only if `p` is congruent to 1 or 3 modulo 8.
|
legendreSym.at_neg_two
theorem legendreSym.at_neg_two : ∀ {p : ℕ} [inst : Fact p.Prime], p ≠ 2 → legendreSym p (-2) = ZMod.χ₈' ↑p
This theorem states that for a natural number `p` which is not equal to 2 and is prime, the Legendre symbol of `p` and `-2` is equal to the second primitive quadratic character on `ZMod 8` evaluated at `p`. The Legendre symbol `legendreSym p (-2)` gives the remainder of `-2` modulo `p`, while `ZMod.χ₈' ↑p` is a function that maps integers to integers based on an array operation in the field of `ZMod 8`.
More concisely: For a prime natural number `p` not equal to 2, the Legendre symbol `legendreSym p (-2)` equals the value of the second primitive quadratic character `ZMod.χ₈'` on `ZMod 8` at `p`.
|
legendreSym.quadratic_reciprocity_one_mod_four
theorem legendreSym.quadratic_reciprocity_one_mod_four :
∀ {p q : ℕ} [inst : Fact p.Prime] [inst_1 : Fact q.Prime],
p % 4 = 1 → q ≠ 2 → legendreSym q ↑p = legendreSym p ↑q
The theorem `legendreSym.quadratic_reciprocity_one_mod_four` is the Law of Quadratic Reciprocity which states that for any two odd prime numbers `p` and `q` where `p` modulo 4 equals 1 and `q` is not equal to 2, the Legendre symbol of `p` and `q` is the same as the Legendre symbol of `q` and `p`. In mathematical terms, this can be represented as `(q / p) = (p / q)` where `/` represents the Legendre symbol.
More concisely: For odd primes p and q with p ≡ 1 (mod 4) and q ≠ 2, the Legendre symbols (p/q) and (q/p) are equal.
|
legendreSym.quadratic_reciprocity_three_mod_four
theorem legendreSym.quadratic_reciprocity_three_mod_four :
∀ {p q : ℕ} [inst : Fact p.Prime] [inst_1 : Fact q.Prime],
p % 4 = 3 → q % 4 = 3 → legendreSym q ↑p = -legendreSym p ↑q
The theorem `legendreSym.quadratic_reciprocity_three_mod_four` is a statement of the Law of Quadratic Reciprocity in the specific case where both prime numbers `p` and `q` are congruent to `3` modulo `4`. It states that, given prime numbers `p` and `q` where `p ≡ 3 (mod 4)` and `q ≡ 3 (mod 4)`, the Legendre symbol `(q / p)` is equal to the negation of the Legendre symbol `(p / q)`. The Legendre symbol `(a / p)` gives the possible residues of `a` modulo `p` and is defined to be `0` if `a ≡ 0 (mod p)`, `1` if `a` is a nonzero square modulo `p` and `-1` otherwise.
More concisely: For prime numbers p and q congruent to 3 modulo 4, the Legendre symbols (q / p) and (p / q) have opposite values.
|