legendreSym.eq_one_or_neg_one
theorem legendreSym.eq_one_or_neg_one :
∀ (p : ℕ) [inst : Fact p.Prime] {a : ℤ}, ↑a ≠ 0 → legendreSym p a = 1 ∨ legendreSym p a = -1
The theorem states that, for any prime number `p` and integer `a`, if `p` does not divide `a` (i.e., `a` is not zero modulo `p`), then the value of the Legendre symbol of `p` and `a` is either `1` or `-1`. This means that `a` is a nonzero square modulo `p` (in which case the Legendre symbol is `1`) or `a` is not a square modulo `p` (in which case the Legendre symbol is `-1`).
More concisely: For any prime number `p` and integer `a` not divisible by `p`, the Legendre symbol of `p` and `a` is equal to either 1 or -1.
|
ZMod.euler_criterion_units
theorem ZMod.euler_criterion_units :
∀ (p : ℕ) [inst : Fact p.Prime] (x : (ZMod p)ˣ), (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1
This theorem is known as Euler's Criterion in the field of number theory. It states that for any prime number `p` and any unit `x` of the integers modulo `p` (`ZMod p`), there exists a number `y` such that `y` squared equals `x` if and only if `x` raised to the power of `p / 2` equals 1. In other words, it provides a test for whether an element is a quadratic residue modulo a prime.
More concisely: For a prime number `p` and any unit `x` in `ZMod p`, `x` is a quadratic residue modulo `p` if and only if `x^(p/2)` equals 1 in `ZMod p`.
|
legendreSym.at_neg_one
theorem legendreSym.at_neg_one : ∀ {p : ℕ} [inst : Fact p.Prime], p ≠ 2 → legendreSym p (-1) = ZMod.χ₄ ↑p
The theorem `legendreSym.at_neg_one` states that for any natural number `p` that is not equal to 2 and is prime, the Legendre symbol of `p` and `-1` is equal to `χ₄ p`. In other words, the Legendre symbol, which indicates the quadratic residue status of `-1` modulo `p`, is given by the value of the nontrivial quadratic character on `ZMod 4`, `χ₄`, at `p`. This character corresponds to the extension `ℚ(√-1)/ℚ`.
More concisely: For a prime natural number `p` not equal to 2, the Legendre symbol of `-1` modulo `p` equals the value of the quadratic character `χ₄` at `p`.
|
legendreSym.eq_one_of_sq_sub_mul_sq_eq_zero'
theorem legendreSym.eq_one_of_sq_sub_mul_sq_eq_zero' :
∀ {p : ℕ} [inst : Fact p.Prime] {a : ℤ},
↑a ≠ 0 → ∀ {x y : ZMod p}, x ≠ 0 → x ^ 2 - ↑a * y ^ 2 = 0 → legendreSym p a = 1
This theorem states that for any prime number `p` and any integer `a` such that `a` is not equal to zero, if there exist numbers `x` and `y` in the integers modulo `p` (denoted `ℤ/pℤ`) such that `x` is not equal to zero and the equation `x^2 - a*y^2 = 0` holds, then the Legendre symbol of `p` and `a`, denoted `legendreSym p a`, is equal to `1`. In other words, if `a` is a nonzero square modulo `p`, then `legendreSym p a = 1`.
More concisely: If `p` is a prime number and `a` is a non-zero integer in `ℤ/pℤ` such that `x^2 = a*y^2` has a solution `x ≠ 0` in `ℤ/pℤ`, then `legendreSym p a = 1`.
|
legendreSym.eq_zero_iff
theorem legendreSym.eq_zero_iff : ∀ (p : ℕ) [inst : Fact p.Prime] (a : ℤ), legendreSym p a = 0 ↔ ↑a = 0
The theorem `legendreSym.eq_zero_iff` states that for any prime number `p` and any integer `a`, the Legendre symbol of `p` and `a` is zero if and only if `p` divides `a`. In other words, if `p` is a factor of `a`, then the Legendre symbol of `p` and `a` will be zero; conversely, if the Legendre symbol of `p` and `a` is zero, then `p` is a factor of `a`.
More concisely: The Legendre symbol of prime number `p` and integer `a` is zero if and only if `p` divides `a`.
|
legendreSym.sq_one
theorem legendreSym.sq_one : ∀ (p : ℕ) [inst : Fact p.Prime] {a : ℤ}, ↑a ≠ 0 → legendreSym p a ^ 2 = 1
The theorem `legendreSym.sq_one` states that for any prime number `p` and any integer `a` such that `a` is not divisible by `p` (i.e., `a ≠ 0` modulo `p`), the square of the Legendre symbol of `a` and `p` is equal to 1. The Legendre symbol is a function that maps integers to {-1, 0, 1}, depending on the properties of `a` modulo `p`: it is 0 if `a` is 0 modulo `p`, 1 if `a` is a nonzero square modulo `p`, and -1 otherwise.
More concisely: For any prime number p and integer a not congruent to 0 modulo p, the Legendre symbol of a and p squared equals 1.
|
legendreSym.eq_zero_mod_of_eq_neg_one
theorem legendreSym.eq_zero_mod_of_eq_neg_one :
∀ {p : ℕ} [inst : Fact p.Prime] {a : ℤ},
legendreSym p a = -1 → ∀ {x y : ZMod p}, x ^ 2 - ↑a * y ^ 2 = 0 → x = 0 ∧ y = 0
The theorem, `legendreSym.eq_zero_mod_of_eq_neg_one`, states that for a prime number `p` and an integer `a`, if the Legendre symbol of `p` and `a` is `-1`, then the only solution of the equation `x^2 - a*y^2 = 0` in the integers modulo `p` (`ℤ/pℤ`) is the trivial solution where both `x` and `y` are equal to zero. In other words, this theorem asserts that if a number is a non-residue modulo a prime (as indicated by the Legendre symbol being `-1`), then its corresponding quadratic equation can only be zeroed by the zero solutions.
More concisely: If the Legendre symbol of a prime number `p` and an integer `a` is `-1`, then there are no non-zero solutions to the congruence `x^2 ≡ a*y^2 (mod p)`.
|
legendreSym.prime_dvd_of_eq_neg_one
theorem legendreSym.prime_dvd_of_eq_neg_one :
∀ {p : ℕ} [inst : Fact p.Prime] {a : ℤ},
legendreSym p a = -1 → ∀ {x y : ℤ}, ↑p ∣ x ^ 2 - a * y ^ 2 → ↑p ∣ x ∧ ↑p ∣ y
The theorem states that for any prime number `p` and any integer `a`, if the Legendre symbol of `p` and `a` is `-1`, and `p` divides the difference of the square of an integer `x` and the product of `a` and the square of another integer `y`, then `p` must divide both `x` and `y`. In other words, if the Legendre symbol of a prime and an integer is `-1` and the prime divides the difference between the square of an integer and the product of the integer and the square of another integer, then the prime must divide both integers. It's an important result in number theory, related to the properties of prime numbers and quadratic residues.
More concisely: If a prime number `p` and integer `a` have a Legendre symbol of `-1`, and `p` divides `x^2 - a*y^2`, then `p` divides both `x` and `y`.
|
ZMod.euler_criterion
theorem ZMod.euler_criterion : ∀ (p : ℕ) [inst : Fact p.Prime] {a : ZMod p}, a ≠ 0 → (IsSquare a ↔ a ^ (p / 2) = 1)
Euler's Criterion is stated in this theorem for a prime number `p` and a nonzero element `a` of the integers modulo `p` (`ZMod p`). The theorem specifies that `a` is a square (i.e., there exists some `r` such that `a` equals `r` times `r`) if and only if `a` raised to the power of `p / 2` equals `1`. This principle in number theory provides a characterization of quadratic residues modulo a prime number.
More concisely: A nonzero integer `a` modulo a prime number `p` is a square if and only if `a^(p/2)` equals 1 in the integers modulo `p`.
|
legendreSym.mul
theorem legendreSym.mul :
∀ (p : ℕ) [inst : Fact p.Prime] (a b : ℤ), legendreSym p (a * b) = legendreSym p a * legendreSym p b
The theorem states that the Legendre symbol is multiplicative with respect to the integer 'a' when a prime number 'p' is kept fixed. In other words, for a given prime number 'p', the Legendre symbol of the product of two integers 'a' and 'b' is equal to the product of the Legendre symbols of 'a' and 'b'. This is formally expressed as `legendreSym p (a * b) = legendreSym p a * legendreSym p b` for all integers 'a' and 'b', and prime number 'p'.
More concisely: For all prime numbers p, the Legendre symbol of the product of two integers a and b is equal to the product of the Legendre symbols of a and b: legendreSym p (a * b) = legendreSym p a * legendreSym p b.
|
legendreSym.sq_one'
theorem legendreSym.sq_one' : ∀ (p : ℕ) [inst : Fact p.Prime] {a : ℤ}, ↑a ≠ 0 → legendreSym p (a ^ 2) = 1
The theorem `legendreSym.sq_one'` states that for any prime number `p` and an integer `a`, if `p` does not divide `a` (i.e., `a` is not zero modulo `p`), then the Legendre symbol of `a^2` at `p` is `1`. In other words, `a^2` is considered a non-zero square modulo `p` if `p` does not divide `a`.
More concisely: For any prime number p and integer a not congruent to zero modulo p, the Legendre symbol of a^2 is equal to 1.
|
ZMod.pow_div_two_eq_neg_one_or_one
theorem ZMod.pow_div_two_eq_neg_one_or_one :
∀ (p : ℕ) [inst : Fact p.Prime] {a : ZMod p}, a ≠ 0 → a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
The theorem `ZMod.pow_div_two_eq_neg_one_or_one` states that for any prime number `p` and any nonzero value `a` in the integers modulo `p`, the value of `a` raised to the power of `p` divided by 2 is either `1` or `-1`. This theorem is applicable in the field of modular arithmetic, specifically when working with the properties of prime numbers and powers in modular integers.
More concisely: For any prime number `p` and nonzero integer `a` modulo `p`, `a^p % 2 = 1` or `a^p % 2 = -1`.
|
legendreSym.eq_one_iff
theorem legendreSym.eq_one_iff :
∀ (p : ℕ) [inst : Fact p.Prime] {a : ℤ}, ↑a ≠ 0 → (legendreSym p a = 1 ↔ IsSquare ↑a)
This theorem states that for any natural number `p` which is prime and any integer `a`, given that `a` is not divisible by `p` (i.e., `a` is not `0` modulo `p`), the Legendre symbol of `p` and `a` equals `1` if and only if `a` is a square modulo `p`. In mathematical terms, if $p$ does not divide $a$, the Legendre symbol $(\frac{a}{p}) = 1$ if and only if $a$ is a quadratic residue modulo $p$.
More concisely: The Legendre symbol of a prime number `p` and an integer `a` not divisible by `p` equals 1 if and only if `a` is a quadratic residue modulo `p`.
|
legendreSym.mod
theorem legendreSym.mod : ∀ (p : ℕ) [inst : Fact p.Prime] (a : ℤ), legendreSym p a = legendreSym p (a % ↑p)
The theorem `legendreSym.mod` states that for any prime number `p` and any integer `a`, the Legendre symbol of `p` and `a`, denoted by `legendreSym p a`, is preserved under modulo operation by `p`. In other words, the value of the Legendre symbol of `p` and `a` is the same as the Legendre symbol of `p` and the remainder of `a` divided by `p` (i.e., `a mod p`). This essentially means that the Legendre symbol only depends on the residue class of `a` modulo `p`, not the specific value of `a`.
More concisely: The Legendre symbol of a prime number `p` and an integer `a` is equal to the Legendre symbol of `p` and the residue of `a` modulo `p`.
|
legendreSym.eq_one_of_sq_sub_mul_sq_eq_zero
theorem legendreSym.eq_one_of_sq_sub_mul_sq_eq_zero :
∀ {p : ℕ} [inst : Fact p.Prime] {a : ℤ},
↑a ≠ 0 → ∀ {x y : ZMod p}, y ≠ 0 → x ^ 2 - ↑a * y ^ 2 = 0 → legendreSym p a = 1
The theorem `legendreSym.eq_one_of_sq_sub_mul_sq_eq_zero` states that for any prime number `p` and any integer `a` that is not equivalent to zero modulo `p`, if there exist numbers `x` and `y` in the integers modulo `p` such that `y` is not zero and the equation `x^2 - a*y^2 = 0` holds, then the Legendre symbol of `p` and `a`, `legendreSym p a`, is equal to `1`. This essentially means that `a` is a nonzero square modulo `p`.
More concisely: If `p` is a prime number, `a` is not congruent to zero modulo `p`, and there exist integers `x` and `y` (not both zero) modulo `p` such that `x^2 ≡ a*y^2 (mod p)`, then `legendreSym p a = 1`.
|
ZMod.exists_sq_eq_neg_one_iff
theorem ZMod.exists_sq_eq_neg_one_iff : ∀ {p : ℕ} [inst : Fact p.Prime], IsSquare (-1) ↔ p % 4 ≠ 3
The theorem `ZMod.exists_sq_eq_neg_one_iff` states that for any prime number `p`, `-1` is a square in the integers modulo `p` if and only if `p` is not congruent to `3` modulo `4`. In other words, there exists an element in the ring of integers modulo `p` whose square equals `-1` if and only if `p` does not leave a remainder of `3` when divided by `4`.
More concisely: For a prime number p in Z, there exists an integer x such that x^2 ≡ -1 (mod p) if and only if p ≡ 1 (mod 4).
|
legendreSym.eq_neg_one_iff
theorem legendreSym.eq_neg_one_iff : ∀ (p : ℕ) [inst : Fact p.Prime] {a : ℤ}, legendreSym p a = -1 ↔ ¬IsSquare ↑a := by
sorry
The theorem `legendreSym.eq_neg_one_iff` states that for any prime number `p` and integer `a`, the Legendre symbol of `p` and `a` equals `-1` if and only if `a` is not a square modulo `p`. In other words, `a` does not satisfy the condition `a = r * r` for some `r` within the modular arithmetic of `p`. This theorem provides a direct way to check whether an integer is a non-square modulo a prime number using the Legendre symbol.
More concisely: The Legendre symbol of a prime number `p` and an integer `a` equals `-1` if and only if `a` is not a square modulo `p`.
|
legendreSym.card_sqrts
theorem legendreSym.card_sqrts :
∀ (p : ℕ) [inst : Fact p.Prime], p ≠ 2 → ∀ (a : ℤ), ↑{x | x ^ 2 = ↑a}.toFinset.card = legendreSym p a + 1 := by
sorry
The theorem `legendreSym.card_sqrts` states that for any natural number `p` which is prime and not equal to 2, and for any integer `a`, the number of square roots of `a` modulo `p` is determined by the Legendre symbol of `a` and `p` plus 1. In other words, the cardinality of the set of all `x` such that `x` squared equals `a` is equal to the value of the Legendre symbol of `a` and `p` plus 1. The Legendre symbol is a function from integers to integers that takes `a` and a prime `p` and returns `0` if `a` is `0` modulo `p`, `1` if `a` is a nonzero square modulo `p`, and `-1` otherwise.
More concisely: For any prime number p different from 2 and any integer a, the number of solutions x to the congruence x^2 ≡ a (mod p) is given by the Legendre symbol (a, p) + 1.
|
legendreSym.eq_pow
theorem legendreSym.eq_pow : ∀ (p : ℕ) [inst : Fact p.Prime] (a : ℤ), ↑(legendreSym p a) = ↑a ^ (p / 2)
The theorem `legendreSym.eq_pow` states that for any natural number `p` that is prime, and any integer `a`, the Legendre symbol of `a` and `p` is congruent to `a` raised to the power of half of `p`, modulo `p`. In other words, it establishes the equivalence between the Legendre symbol and a particular power of `a`, under modular arithmetic with `p`. In mathematical notation, this is expressed as `legendreSym(p, a) ≡ a ^ (p / 2) mod p`.
More concisely: For any prime number `p` and integer `a`, the Legendre symbol `legendreSym(p, a)` equals `a` raised to the power of `p/2` modulo `p`.
|
ZMod.mod_four_ne_three_of_sq_eq_neg_sq'
theorem ZMod.mod_four_ne_three_of_sq_eq_neg_sq' :
∀ {p : ℕ} [inst : Fact p.Prime] {x y : ZMod p}, y ≠ 0 → x ^ 2 = -y ^ 2 → p % 4 ≠ 3
This theorem states that for any prime number `p` and any two nonzero elements `x` and `y` of the integers modulo `p` (denoted `ZMod p`), if the square of `x` is equal to the negative of the square of `y`, then `p` cannot be congruent to `3` modulo `4`. The theorem reflects a condition under which a prime number cannot have a certain remainder when divided by `4` given certain properties of elements in its corresponding modular arithmetic system.
More concisely: If `p` is a prime number and `x, y` are nonzero elements of `ZMod p` such that `x^2 = -y^2`, then `p` is not congruent to 3 modulo 4.
|