jacobiSym.mod_left'
theorem jacobiSym.mod_left' : ∀ {a₁ a₂ : ℤ} {b : ℕ}, a₁ % ↑b = a₂ % ↑b → jacobiSym a₁ b = jacobiSym a₂ b
This theorem states that the Jacobi symbol `J(a | b)` depends only on the modulo `b` of `a`. More specifically, for any integers `a₁` and `a₂` and a natural number `b` if `a₁` modulo `b` equals `a₂` modulo `b`, then the Jacobi symbol of `a₁` and `b` equals the Jacobi symbol of `a₂` and `b`. In other words, the value of the Jacobi symbol does not change if `a` is replaced by another integer equivalent to it modulo `b`. This property aligns with the fact that the Jacobi symbol is a generalization of the Legendre symbol, which also has this modular property.
More concisely: The Jacobi symbol is multiplicatively symmetric modulo a composite number b, that is, J(a₁ | b) = J(a₂ | b) if a₁ ≡ a₂ (mod b).
|
qrSign.neg_one_pow
theorem qrSign.neg_one_pow : ∀ {m n : ℕ}, Odd m → Odd n → qrSign m n = (-1) ^ (m / 2 * (n / 2))
The theorem `qrSign.neg_one_pow` states that for any two natural numbers, `m` and `n`, if both `m` and `n` are odd (where a number is defined as odd if it can be expressed in the form `2k + 1` for some `k`), then the value of the bi-multiplicative map `qrSign` at `m` and `n` can be expressed as `-1` raised to the power of `m / 2 * n / 2`. This theorem relates the quadratic reciprocity sign to the parity of numbers.
More concisely: For odd natural numbers m and n, the value of the bi-multiplicative map qrSign is equal to -1 raised to the power of (m / 2 * n / 2).
|
jacobiSym.at_neg_two
theorem jacobiSym.at_neg_two : ∀ {b : ℕ}, Odd b → jacobiSym (-2) b = ZMod.χ₈' ↑b
The theorem `jacobiSym.at_neg_two` states that for any natural number `b` which is odd (meaning there exists some `k` such that `b = 2*k + 1`), the Jacobi symbol of `-2` and `b`, denoted as `J(-2 | b)`, is equal to the second primitive quadratic character on `ZMod 8`, `χ₈' b`. This character is associated with the extension `ℚ(√-2)/ℚ`. In other words, if `b` is an odd number, then the Jacobi symbol of `-2` and `b` is given by applying `χ₈'` to `b`.
More concisely: For any odd natural number `b`, the Jacobi symbol of `-2` and `b` equals the second primitive quadratic character `χ₈'` evaluated at `b`.
|
jacobiSym.quadratic_reciprocity
theorem jacobiSym.quadratic_reciprocity :
∀ {a b : ℕ}, Odd a → Odd b → jacobiSym (↑a) b = (-1) ^ (a / 2 * (b / 2)) * jacobiSym (↑b) a
The Law of Quadratic Reciprocity for the Jacobi symbol states that for any two natural numbers `a` and `b` which are both odd, the Jacobi symbol of `a` and `b` equals `-1` raised to the power of the product of `a` and `b` divided by 4 (or equivalently, `a` divided by 2 times `b` divided by 2), times the Jacobi symbol of `b` and `a`. In mathematical notation, for odd `a` and `b`, `jacobiSym(a, b) = (-1)^(a/2 * b/2) * jacobiSym(b, a)`.
More concisely: For odd integers a and b, the Jacobi symbol of a and b is equal to (-1)^{(a-1)/2 \* (b-1)/2 \* (jacobiSym of b, a)}.
|
jacobiSym.mul_right
theorem jacobiSym.mul_right :
∀ (a : ℤ) (b₁ b₂ : ℕ) [inst : NeZero b₁] [inst : NeZero b₂],
jacobiSym a (b₁ * b₂) = jacobiSym a b₁ * jacobiSym a b₂
This theorem states that the Jacobi symbol has the multiplicative property with respect to its second argument. Specifically, for any integer `a` and non-zero natural numbers `b₁` and `b₂`, the Jacobi symbol of `a` and the product of `b₁` and `b₂` is equal to the product of the Jacobi symbol of `a` and `b₁` and the Jacobi symbol of `a` and `b₂`. In mathematical terms, we can express this as: if `b₁ ≠ 0` and `b₂ ≠ 0`, then `jacobiSym(a, b₁ * b₂) = jacobiSym(a, b₁) * jacobiSym(a, b₂)`.
More concisely: For any integer `a` and non-zero natural numbers `b₁` and `b₂`, the Jacobi symbol `jacobiSym(a, b₁ * b₂)` equals the product of `jacobiSym(a, b₁)` and `jacobiSym(a, b₂)`.
|
qrSign.sq_eq_one
theorem qrSign.sq_eq_one : ∀ {m n : ℕ}, Odd m → Odd n → qrSign m n ^ 2 = 1
The theorem `qrSign.sq_eq_one` states that for any two natural numbers `m` and `n` that are both odd, the square of the bi-multiplicative map (`qrSign`) applied to `m` and `n` equals `1`. In other words, if `m` and `n` are odd numbers (thus there exist integers `k` and `l` such that `m = 2*k + 1` and `n = 2*l + 1`), then the quantity `(qrSign m n)^2` is equal to `1`. Here, `qrSign` is defined as the Jacobi symbol of the fourth primitive root of unity applied to `m` and multiplied by `n`, operating within the ring of integers.
More concisely: For odd natural numbers m and n, the square of the Jacobi symbol of the fourth root of unity applied to m and multiplied by n equals 1.
|
qrSign.mul_left
theorem qrSign.mul_left : ∀ (m₁ m₂ n : ℕ), qrSign (m₁ * m₂) n = qrSign m₁ n * qrSign m₂ n
The theorem `qrSign.mul_left` states that the function `qrSign`, which represents the bi-multiplicative map that gives the sign in the Law of Quadratic Reciprocity, is multiplicative in its first argument. Specifically, for any three natural numbers `m₁`, `m₂`, and `n`, the value of `qrSign` at the product of `m₁` and `m₂` and `n` is equal to the product of `qrSign` at `m₁` and `n` and `qrSign` at `m₂` and `n`.
More concisely: The theorem `qrSign.mul_left` asserts that for all natural numbers m₁, m₂, and n, qrSign(m₁ * m₂ * n) = qrSign(m₁ * n) * qrSign(m₂ * n).
|
jacobiSym.ne_zero
theorem jacobiSym.ne_zero : ∀ {a : ℤ} {b : ℕ}, a.gcd ↑b = 1 → jacobiSym a b ≠ 0
The theorem `jacobiSym.ne_zero` states that for all integers `a` and natural numbers `b`, if `a` and `b` are coprime (that is, their greatest common divisor is 1), then the Jacobi symbol `J(a | b)` is not equal to zero. The Jacobi symbol `J(a | b)` is computed as the product of the Legendre symbols for each of the prime factors of `b` with `a` as the argument.
More concisely: If integers `a` and `b` are coprime, then the Jacobi symbol `J(a | b)` is non-zero.
|
jacobiSym.eq_zero_iff_not_coprime
theorem jacobiSym.eq_zero_iff_not_coprime : ∀ {a : ℤ} {b : ℕ} [inst : NeZero b], jacobiSym a b = 0 ↔ a.gcd ↑b ≠ 1 := by
sorry
This theorem states that the Jacobi symbol `J(a | b)` is equal to zero if and only if the integers `a` and `b` are not coprime, given that `b` is not equal to zero. Here, two integers are considered to be coprime if their greatest common divisor (gcd) is 1. So essentially, if the gcd of `a` and `b` is not 1, then the Jacobi symbol `J(a | b)` will be zero.
More concisely: The Jacobi symbol J(a | b) equals zero if and only if a and b are not coprime.
|
jacobiSym.quadratic_reciprocity_three_mod_four
theorem jacobiSym.quadratic_reciprocity_three_mod_four :
∀ {a b : ℕ}, a % 4 = 3 → b % 4 = 3 → jacobiSym (↑a) b = -jacobiSym (↑b) a
This theorem is called the Law of Quadratic Reciprocity for the Jacobi symbol. It states that for any two natural numbers `a` and `b` that are both congruent to `3` modulo `4`, the Jacobi symbol `J(a | b)` is equal to the negative of the Jacobi symbol `J(b | a)`. Here, the Jacobi symbol `J(a | b)` is a mathematical function that depends on the prime factors of `b` and is computed by the function `jacobiSym`.
More concisely: For integers `a` and `b` congruent to 3 modulo 4, the Jacobi symbol `J(a | b)` equals the negative of `J(b | a)`.
|
jacobiSym.pow_right
theorem jacobiSym.pow_right : ∀ (a : ℤ) (b e : ℕ), jacobiSym a (b ^ e) = jacobiSym a b ^ e
The theorem `jacobiSym.pow_right` states that for any integer `a`, and any natural numbers `b` and `e`, the Jacobi symbol of `a` and `b` to the power of `e`, denoted as `J(a | b^e)`, is equal to the Jacobi symbol of `a` and `b` itself raised to the power `e`, denoted as `J(a | b)^e`. This means that in the computation of the Jacobi symbol, an exponent in the second argument can be transferred to the outside.
More concisely: The Jacobi symbol of a number with respect to another number raised to an exponent is equal to the product of the Jacobi symbols of the numbers with respect to each other, each raised to the power of the exponent.
|
jacobiSym.at_two
theorem jacobiSym.at_two : ∀ {b : ℕ}, Odd b → jacobiSym 2 b = ZMod.χ₈ ↑b
The theorem `jacobiSym.at_two` states that for any natural number `b` that is odd (in the sense that there exists some integer `k` such that `b = 2*k + 1`), the Jacobi symbol of `2` and `b` is equal to the value of the first primitive quadratic character on `ZMod 8`, denoted `χ₈`, at `b`. In mathematical terms, this can be written as: if `b` is odd, then `J(2 | b) = χ₈(b)`.
More concisely: For any odd natural number `b`, the Jacobi symbol of `2` and `b` equals the value of the first primitive quadratic character modulo 8 at `b`.
|
ZMod.nonsquare_of_jacobiSym_eq_neg_one
theorem ZMod.nonsquare_of_jacobiSym_eq_neg_one : ∀ {a : ℤ} {b : ℕ}, jacobiSym a b = -1 → ¬IsSquare ↑a
This theorem states that for any integer `a` and natural number `b`, if the Jacobi symbol `J(a | b)` equals `-1`, then `a` is not a square modulo `b`. In mathematical terms, if the Jacobi symbol, which is a function used in number theory and defined as the product of the Legendre symbols for the prime factors of `b`, is `-1`, then there does not exist an integer `r` such that `a` is equivalent to `r` squared modulo `b`.
More concisely: If the Jacobi symbol $J(a | b) = -1$, then there is no integer $r$ such that $a \equiv r^2 \pmod{b}$.
|
jacobiSym.one_left
theorem jacobiSym.one_left : ∀ (b : ℕ), jacobiSym 1 b = 1
This theorem states that, for any natural number `b`, the Jacobi symbol `J(1 | b)` is equal to `1`. In other words, when the first argument of the Jacobi symbol function (`jacobiSym`) is `1`, the resulting value of the function is always `1`, regardless of the value of `b`.
More concisely: For all natural numbers b, the Jacobi symbol J(1 | b) equals 1.
|
jacobiSym.pow_left
theorem jacobiSym.pow_left : ∀ (a : ℤ) (e b : ℕ), jacobiSym (a ^ e) b = jacobiSym a b ^ e
The theorem `jacobiSym.pow_left` states that for all integers `a` and natural numbers `e` and `b`, the Jacobi symbol of `a` raised to the power `e` and `b` is equal to the Jacobi symbol of `a` and `b` raised to the power `e`. In mathematical notation, this can be expressed as `J(a^e | b) = J(a | b)^e`, where `J(a | b)` denotes the Jacobi symbol of `a` and `b`.
More concisely: The Jacobi symbol of an integer `a` raised to the power `e` with respect to another integer `b` equals the `e`th power of the Jacobi symbol of `a` and `b`. In symbols: `J(a^e | b) = J(a | b)^e`.
|
jacobiSym.list_prod_right
theorem jacobiSym.list_prod_right :
∀ {a : ℤ} {l : List ℕ}, (∀ n ∈ l, n ≠ 0) → jacobiSym a l.prod = (List.map (fun n => jacobiSym a n) l).prod := by
sorry
This theorem states that for any integer `a` and list of natural numbers `l`, as long as no number `n` in `l` is zero, the Jacobi symbol of `a` and the product of the list `l` is equal to the product of the list obtained by applying the Jacobi symbol to `a` and each number in `l` individually. This is equivalent to saying we can distribute the Jacobi symbol over the product of a list of numbers. In mathematical terms, if $l$ is a list of natural numbers with none of them being zero, then $jacobiSym(a, \prod l) = \prod_{n \in l} jacobiSym(a, n)$.
More concisely: For any integer `a` and non-empty list `l` of natural numbers, the Jacobi symbol of `a` with the product of `l` equals the product of the Jacobi symbols of `a` with each number in `l`.
|
qrSign.mul_right
theorem qrSign.mul_right :
∀ (m n₁ n₂ : ℕ) [inst : NeZero n₁] [inst : NeZero n₂], qrSign m (n₁ * n₂) = qrSign m n₁ * qrSign m n₂
The theorem `qrSign.mul_right` states that the function `qrSign`, which returns the sign in the Law of Quadratic Reciprocity, is multiplicative in its second argument. In other words, for any natural numbers `m`, `n₁`, and `n₂`, with both `n₁` and `n₂` not equal to zero, the result of `qrSign m` applied to the product of `n₁` and `n₂` is equal to the product of the result of `qrSign m` applied to `n₁` and `qrSign m` applied to `n₂`. This is expressed as: $\text{qrSign}(m, n₁ \times n₂) = \text{qrSign}(m, n₁) \times \text{qrSign}(m, n₂)$.
More concisely: For all natural numbers m, n₁, and n₂ not equal to zero, qrSign(m, n₁ * n₂) = qrSign(m, n₁) * qrSign(m, n₂).
|
jacobiSym.zero_right
theorem jacobiSym.zero_right : ∀ (a : ℤ), jacobiSym a 0 = 1
The theorem `jacobiSym.zero_right` asserts that for every integer `a`, the Jacobi symbol `J(a | 0)` is equal to `1`. In other words, if the second argument of the Jacobi symbol is `0`, the symbol always evaluates to `1` regardless of the value of the first argument.
More concisely: For all integers `a`, the Jacobi symbol `J(a | 0)` equals 1.
|
jacobiSym.eq_zero_iff
theorem jacobiSym.eq_zero_iff : ∀ {a : ℤ} {b : ℕ}, jacobiSym a b = 0 ↔ b ≠ 0 ∧ a.gcd ↑b ≠ 1
The theorem states that the Jacobi symbol `J(a | b)` is equal to zero if and only if two conditions are met: firstly, `b` is not equal to zero; and secondly, `a` and `b` are not coprime, meaning that the greatest common divisor (gcd) of `a` and `b` is not 1.
More concisely: The Jacobi symbol J(a | b) equals zero if and only if b is non-zero and a and b are not coprime.
|
jacobiSym.sq_one
theorem jacobiSym.sq_one : ∀ {a : ℤ} {b : ℕ}, a.gcd ↑b = 1 → jacobiSym a b ^ 2 = 1
The theorem `jacobiSym.sq_one` states that for any integer `a` and natural number `b`, if `a` and `b` are coprime (i.e., the greatest common divisor of `a` and `b` is 1), then the square of the Jacobi symbol of `a` and `b`, denoted by `J(a | b)`, is equal to 1. The Jacobi symbol of `a` and `b`, `J(a | b)`, is computed by taking the product of the Legendre symbols of `a` with respect to each prime factor of `b`.
More concisely: If integers `a` and `b` are coprime, then the square of their Jacobi symbol is equal to 1. (i.e., `J(a | b) ^ 2 = 1`).
|
jacobiSym.list_prod_left
theorem jacobiSym.list_prod_left :
∀ {l : List ℤ} {n : ℕ}, jacobiSym l.prod n = (List.map (fun a => jacobiSym a n) l).prod
This theorem states that for any list of integers `l` and a natural number `n`, the Jacobi symbol of the product of `l` and `n` is equal to the product of the list obtained by mapping each integer `a` in `l` to the Jacobi symbol of `a` and `n`. In other words, the Jacobi symbol operation can distribute over the product operation in the first argument, similar to how multiplication distributes over addition.
More concisely: The Jacobi symbol of the product of an integer list and a natural number is equal to the product of the list of Jacobi symbols of each integer with the natural number.
|
jacobiSym.value_at
theorem jacobiSym.value_at :
∀ (a : ℤ) {R : Type u_1} [inst : CommSemiring R] (χ : R →* ℤ),
(∀ (p : ℕ) (pp : p.Prime), p ≠ 2 → legendreSym p a = χ ↑p) → ∀ {b : ℕ}, Odd b → jacobiSym a b = χ ↑b
The theorem `jacobiSym.value_at` states that for any integer `a` and any commutative semiring `R`, if `χ` is a multiplicative function such that the Jacobi symbol `J(a | p)` equals `χ p` for all odd prime numbers `p`, then the Jacobi symbol `J(a | b)` equals `χ b` for all odd natural numbers `b`. In other words, if a multiplicative function `χ` maps odd primes to their corresponding Jacobi symbols with respect to `a`, then this function will also map any odd natural number to its corresponding Jacobi symbol with respect to `a`.
More concisely: If `χ` is a multiplicative function satisfying `J(a | p) = χ p` for all odd prime numbers `p`, then `J(a | b) = χ b` for all odd natural numbers `b`.
|
jacobiSym.mod_right'
theorem jacobiSym.mod_right' : ∀ (a : ℕ) {b : ℕ}, Odd b → jacobiSym (↑a) b = jacobiSym (↑a) (b % (4 * a))
This theorem states that the Jacobi symbol, represented by `J(a | b)`, only depends on the modulo of `b` by `4*a`, when `a` is a natural number. This is under the condition that `b` is an odd number, which means there exists a number `k` such that `b = 2*k + 1`. Therefore, the value of the Jacobi symbol `J(a | b)` is equal to `J(a | (b mod 4*a))`.
More concisely: The Jacobi symbol `J(a | b)` is equal to `J(a | (b mod 4*a))` for odd integers `b`, where `a` is a natural number.
|
jacobiSym.zero_left
theorem jacobiSym.zero_left : ∀ {b : ℕ}, 1 < b → jacobiSym 0 b = 0
This theorem states that, for any natural number `b` greater than 1, the Jacobi symbol `J(0 | b)` is equal to zero. In other words, whenever we evaluate the Jacobi symbol with the first argument being zero and the second argument being a natural number greater than one, the result will always be zero.
More concisely: For any natural number `b` greater than 1, the Jacobi symbol `J(0 | b)` equals zero.
|
jacobiSym.quadratic_reciprocity'
theorem jacobiSym.quadratic_reciprocity' :
∀ {a b : ℕ}, Odd a → Odd b → jacobiSym (↑a) b = qrSign b a * jacobiSym (↑b) a
The theorem `jacobiSym.quadratic_reciprocity'` states the Law of Quadratic Reciprocity for the Jacobi symbol, using the function `qrSign`. Specifically, it applies to any two natural numbers `a` and `b` that are both odd. The theorem asserts that the Jacobi symbol of `a` and `b`, denoted as `jacobiSym (↑a) b`, is equal to the product of `qrSign b a` (the sign given by the Law of Quadratic Reciprocity) and `jacobiSym (↑b) a` (the Jacobi symbol of `b` and `a`).
More concisely: For odd integers a and b, the Jacobi symbols jacobiSym (a) b and jacobiSym (b) a are equal to the product of qrSign b a and jacobiSym (a) b, according to the Law of Quadratic Reciprocity.
|
jacobiSym.one_right
theorem jacobiSym.one_right : ∀ (a : ℤ), jacobiSym a 1 = 1
The theorem `jacobiSym.one_right` states that for any integer `a`, the Jacobi symbol `J(a | 1)`, where `J` is denoted by `jacobiSym` function in Lean 4, is equal to `1`. In mathematical terms, this theorem says that the Jacobi symbol of any integer `a` and `1` is always `1`.
More concisely: For all integers `a`, the Jacobi symbol `J(a | 1)` equals 1.
|
jacobiSym.prime_dvd_of_eq_neg_one
theorem jacobiSym.prime_dvd_of_eq_neg_one :
∀ {p : ℕ} [inst : Fact p.Prime] {a : ℤ},
jacobiSym a p = -1 → ∀ {x y : ℤ}, ↑p ∣ x ^ 2 - a * y ^ 2 → ↑p ∣ x ∧ ↑p ∣ y
The theorem `jacobiSym.prime_dvd_of_eq_neg_one` states that for any prime number `p`, and any integers `a`, `x`, and `y`, if the Jacobi symbol of `a` and `p` equals `-1`, and `p` divides `x^2 - a*y^2`, then `p` must also divide both `x` and `y`. This is a statement about prime numbers and properties of divisibility in relation to the Jacobi symbol, which is a function in number theory used to generalize the Legendre symbol.
More concisely: If a prime number p, an integer a having Jacobi symbol -1 modulo p, and integers x and y are such that p divides x^2 - a*y^2, then p divides both x and y.
|
jacobiSym.mul_left
theorem jacobiSym.mul_left : ∀ (a₁ a₂ : ℤ) (b : ℕ), jacobiSym (a₁ * a₂) b = jacobiSym a₁ b * jacobiSym a₂ b
The theorem `jacobiSym.mul_left` states that the Jacobi symbol is multiplicative in its first argument. In other words, for any two integers `a₁` and `a₂` and a natural number `b`, the Jacobi symbol of the product of `a₁` and `a₂` with respect to `b` is equal to the product of the Jacobi symbol of `a₁` with respect to `b` and the Jacobi symbol of `a₂` with respect to `b`. This property is a key aspect of the Jacobi symbol's behavior and is analogous to the multiplicativity property in other number-theoretical functions like the Legendre symbol and the Möbius function.
More concisely: The Jacobi symbol is multiplicative in its first argument, i.e., for integers `a₁`, `a₂`, and a natural number `b`, `(a₁ * a₂) % b ≡ (a₁ % b) * (a₂ % b) (mod p)`.
|
jacobiSym.neg
theorem jacobiSym.neg : ∀ (a : ℤ) {b : ℕ}, Odd b → jacobiSym (-a) b = ZMod.χ₄ ↑b * jacobiSym a b
This theorem states that for any integer `a` and any natural number `b` that is odd (i.e., there exists some `k` such that `b = 2*k + 1`), the Jacobi symbol of `-a` and `b` equals the product of the nontrivial quadratic character on `ZMod 4` of `b` and the Jacobi symbol of `a` and `b`. In other words, `J(-a | b) = χ₄ b * J(a | b)`. This theorem is related to the properties of quadratic reciprocity in number theory.
More concisely: For any integer `a` and odd natural number `b`, the Jacobi symbol `J(-a | b)` equals the product of the nontrivial quadratic character `χ₄` of `b` and the Jacobi symbol `J(a | b)`.
|
jacobiSym.mod_left
theorem jacobiSym.mod_left : ∀ (a : ℤ) (b : ℕ), jacobiSym a b = jacobiSym (a % ↑b) b
The theorem `jacobiSym.mod_left` states that the Jacobi symbol `J(a | b)` of an integer `a` and a positive natural number `b` depends only on the modulus of `a` by `b`. In other words, the Jacobi symbol remains unchanged if `a` is replaced by the remainder of `a` divided by `b`.
More concisely: The Jacobi symbol of an integer with respect to a positive integer is invariant under taking the remainder modulo that integer.
|
jacobiSym.legendreSym.to_jacobiSym
theorem jacobiSym.legendreSym.to_jacobiSym : ∀ (p : ℕ) [fp : Fact p.Prime] (a : ℤ), legendreSym p a = jacobiSym a p
The theorem `jacobiSym.legendreSym.to_jacobiSym` states that for any prime number `p` and any integer `a`, the Legendre symbol `legendreSym p a` is equal to the Jacobi symbol `jacobiSym a p`. In other words, the Legendre symbol, which evaluates to `0` if `a` is `0` modulo `p`, `1` if `a` is a nonzero square modulo `p`, or `-1` otherwise, is identical to the Jacobi symbol which uses the same Legendre symbol values for each prime factor of `p`.
More concisely: The Legendre symbol and Jacobi symbol agree in value for any prime number `p` and integer `a`.
|
jacobiSym.quadratic_reciprocity_one_mod_four
theorem jacobiSym.quadratic_reciprocity_one_mod_four :
∀ {a b : ℕ}, a % 4 = 1 → Odd b → jacobiSym (↑a) b = jacobiSym (↑b) a
This theorem asserts the Law of Quadratic Reciprocity for the Jacobi symbol. Specifically, it states that for any natural numbers `a` and `b`, if `a` is congruent to 1 modulo 4 and `b` is an odd number, then the Jacobi symbol of `a` and `b` is equal to the Jacobi symbol of `b` and `a`. In mathematical notation, this can be expressed as: if $a \equiv 1 \mod 4$ and $b$ is odd, then $J(a | b) = J(b | a)$, where $J$ denotes the Jacobi symbol. The Jacobi symbol, denoted $J(a | b)$, is a product of Legendre symbols for each prime factor of $b$. An element of a semiring is called odd if it can be expressed as $2k + 1$ for some integer $k$.
More concisely: If both `a` and `b` are odd natural numbers with `a` congruent to 1 modulo 4, then the Jacobi symbols of `a` and `b` are equal: `J(a | b) = J(b | a)`.
|
jacobiSym.trichotomy
theorem jacobiSym.trichotomy : ∀ (a : ℤ) (b : ℕ), jacobiSym a b = 0 ∨ jacobiSym a b = 1 ∨ jacobiSym a b = -1
The theorem `jacobiSym.trichotomy` asserts that for any integer `a` and natural number `b`, the Jacobi symbol of `a` and `b`, as defined by the `jacobiSym` function, can assume only one of three possible values: `0`, `1`, or `-1`. In mathematical terms, the theorem states that for all $a \in \mathbb{Z}$ and $b \in \mathbb{N}$, we have $\text{jacobiSym}(a, b) \in \{0, 1, -1\}$.
More concisely: For all integers $a$ and natural numbers $b$, the Jacobi symbol $\text{jacobiSym}(a, b)$ takes on one of the values $0, 1,$ or $-1$.
|
jacobiSym.sq_one'
theorem jacobiSym.sq_one' : ∀ {a : ℤ} {b : ℕ}, a.gcd ↑b = 1 → jacobiSym (a ^ 2) b = 1
This theorem states that for any integer `a` and any natural number `b`, if `a` and `b` are coprime (i.e., the greatest common divisor of `a` and `b` is 1), then the Jacobi symbol of `a` squared and `b`, denoted J(a^2 | b), is equal to 1. In other words, when `a` and `b` share no common factors other than 1, squaring `a` and using it in the computation of the Jacobi symbol with `b` results in a value of 1.
More concisely: For any integers `a` and `b`, if `gcd(a, b) = 1`, then `J(a^2 | b) = 1`, where `J` denotes the Jacobi symbol.
|
ZMod.isSquare_of_jacobiSym_eq_one
theorem ZMod.isSquare_of_jacobiSym_eq_one : ∀ {a : ℤ} {p : ℕ} [inst : Fact p.Prime], jacobiSym a p = 1 → IsSquare ↑a
This theorem states that for any integer `a` and any prime number `p`, if `p` is indeed a prime number (verified by the `Fact` instance) and the Jacobi symbol of `a` and `p` equals 1, then `a` is a perfect square modulo `p`. In other words, there exists an integer `r` such that `a` is congruent to the square of `r` modulo `p`.
More concisely: For any integer `a` and prime number `p` with `p` verified as prime and the Jacobi symbol of `a` and `p` equal to 1, there exists an integer `r` such that `a` is congruent to the square of `r` modulo `p`.
|
jacobiSym.eq_one_or_neg_one
theorem jacobiSym.eq_one_or_neg_one : ∀ {a : ℤ} {b : ℕ}, a.gcd ↑b = 1 → jacobiSym a b = 1 ∨ jacobiSym a b = -1 := by
sorry
The theorem `jacobiSym.eq_one_or_neg_one` states that for any two numbers `a` and `b`, where `a` is an integer and `b` is a natural number, if `a` and `b` are coprime (i.e., the greatest common divisor of `a` and `b` is 1), then the Jacobi symbol of `a` and `b`, denoted as `J(a | b)`, is either `1` or `-1`.
More concisely: If integers `a` and `b` are coprime, then the Jacobi symbol `J(a | b)` equals `1` or `-1`.
|
jacobiSym.mod_right
theorem jacobiSym.mod_right : ∀ (a : ℤ) {b : ℕ}, Odd b → jacobiSym a b = jacobiSym a (b % (4 * a.natAbs))
This theorem states that the Jacobi symbol `J(a | b)`, denoted in Lean as `jacobiSym a b`, is only dependent on `b` modulo `4*a`. In other words, given an integer `a` and a natural number `b` that is odd (that is, there exists a number `k` such that `b = 2*k + 1`), the value of the Jacobi symbol `J(a | b)` is the same as the Jacobi symbol `J(a | b mod 4*a)`. Here, `a.natAbs` represents the absolute value of `a`. Essentially, this theorem is saying that the Jacobi symbol is invariant under the replacement of `b` with `b mod 4*a`, when `b` is odd.
More concisely: For odd integers a and b, the Jacobi symbol jacobiSym a b is equal to jacobiSym a (b mod 4*a).
|
qrSign.symm
theorem qrSign.symm : ∀ {m n : ℕ}, Odd m → Odd n → qrSign m n = qrSign n m
The theorem `qrSign.symm` asserts that the bi-multiplicative map `qrSign`, which is used to represent the sign in the Law of Quadratic Reciprocity, is symmetric for odd numbers. In other words, for any two natural numbers `m` and `n` that are odd (i.e., they can be expressed in the form `2*k + 1` for some integer `k`), the value of `qrSign m n` is equal to the value of `qrSign n m`.
More concisely: For odd integers m and n, the value of qrSign(m, n) equals qrSign(n, m).
|
jacobiSym.eq_neg_one_at_prime_divisor_of_eq_neg_one
theorem jacobiSym.eq_neg_one_at_prime_divisor_of_eq_neg_one :
∀ {a : ℤ} {n : ℕ}, jacobiSym a n = -1 → ∃ p, p.Prime ∧ p ∣ n ∧ jacobiSym a p = -1
The theorem `jacobiSym.eq_neg_one_at_prime_divisor_of_eq_neg_one` states that for any integer `a` and natural number `n`, if the Jacobi symbol `J(a | n)` equals `-1`, then there exists a prime number `p` that divides `n` for which the Jacobi symbol `J(a | p)` also equals `-1`. In other words, if the Jacobi symbol of `a` and `n` is `-1`, then `n` has a prime divisor `p` such that the Jacobi symbol of `a` and `p` is `-1`.
More concisely: If `J(a | n) = -1` in the Jacobi symbol, then there exists a prime divisor `p` of `n` such that `J(a | p) = -1`.
|
qrSign.eq_iff_eq
theorem qrSign.eq_iff_eq : ∀ {m n : ℕ}, Odd m → Odd n → ∀ (x y : ℤ), qrSign m n * x = y ↔ x = qrSign m n * y
This theorem states that for any two natural numbers `m` and `n` that are both odd, for any two integers `x` and `y`, the equality `qrSign m n * x = y` is equivalent to `x = qrSign m n * y`. Here, `qrSign m n` denotes the bi-multiplicative map giving the sign in the Law of Quadratic Reciprocity. The function `Odd` determines if a number is odd by checking if it can be represented as `2*k + 1` for some `k`. In other words, if `m` and `n` are odd numbers, then multiplying `qrSign m n` by `x` to get `y` is the same as having `x` equal to the product of `qrSign m n` and `y`.
More concisely: For odd natural numbers m and n, the equality qrSign m n * x = y holds if and only if x = qrSign m n * y.
|
ZMod.nonsquare_iff_jacobiSym_eq_neg_one
theorem ZMod.nonsquare_iff_jacobiSym_eq_neg_one :
∀ {a : ℤ} {p : ℕ} [inst : Fact p.Prime], jacobiSym a p = -1 ↔ ¬IsSquare ↑a
This theorem states that for a given integer `a` and a natural number `p` where `p` is prime, the Jacobi symbol of `a` and `p` (denoted `J(a | p)`) equals `-1` if and only if `a` is not a square modulo `p`. In other words, `a` not being a perfect square in the ring of integers modulo `p` is equivalent to the Jacobi symbol `J(a | p)` being `-1`.
More concisely: The Jacobi symbol of an integer `a` modulo a prime `p` is `-1` if and only if `a` is not a square modulo `p`.
|
jacobiSym.quadratic_reciprocity_one_mod_four'
theorem jacobiSym.quadratic_reciprocity_one_mod_four' :
∀ {a b : ℕ}, Odd a → b % 4 = 1 → jacobiSym (↑a) b = jacobiSym (↑b) a
The theorem `jacobiSym.quadratic_reciprocity_one_mod_four'` is about the Law of Quadratic Reciprocity of the Jacobi symbol. This law states that if `a` and `b` are natural numbers, and `a` is odd while `b` is congruent to 1 modulo 4, then the Jacobi symbol of `a` and `b` is equal to the Jacobi symbol of `b` and `a`. In other words, under these conditions, the Jacobi symbol is symmetric with respect to its input parameters `a` and `b`. The Jacobi symbol is a generalization of the Legendre symbol, which is a useful tool in number theory for describing quadratic residues.
More concisely: If `a` is an odd natural number and `b` is congruent to 1 modulo 4, then the Jacobi symbol of `a` and `b` equals the Jacobi symbol of `b` and `a`.
|
jacobiSym.at_neg_one
theorem jacobiSym.at_neg_one : ∀ {b : ℕ}, Odd b → jacobiSym (-1) b = ZMod.χ₄ ↑b
This theorem states that for any natural number `b` which is odd, the Jacobi symbol `J(-1 | b)` is equal to the nontrivial quadratic character on `ZMod 4`, denoted as `χ₄ b`. Here, a number is considered odd if it can be represented as `2*k + 1` for some integer `k`, the Jacobi symbol is a certain function of two integers, and `χ₄` is a function mapping integers to the set of integers modulo 4. The Jacobi symbol and `χ₄` function are often used in number theory.
More concisely: For any odd natural number `b`, the Jacobi symbol `J(-1 | b)` equals the nontrivial quadratic character `χ₄` on `ZMod 4`, i.e., `J(-1 | b) = χ₄ b`.
|
jacobiSym.mul_right'
theorem jacobiSym.mul_right' :
∀ (a : ℤ) {b₁ b₂ : ℕ}, b₁ ≠ 0 → b₂ ≠ 0 → jacobiSym a (b₁ * b₂) = jacobiSym a b₁ * jacobiSym a b₂
The theorem `jacobiSym.mul_right'` states that the Jacobi symbol, denoted as `jacobiSym a b` for integers `a` and natural numbers `b`, is multiplicative in its second argument. More specifically, for any integer `a` and non-zero natural numbers `b₁` and `b₂`, the Jacobi symbol of `a` and the product `b₁ * b₂` is equal to the product of the Jacobi symbol of `a` and `b₁` and the Jacobi symbol of `a` and `b₂`. This means that the operation of taking the Jacobi symbol commutes with multiplication on its second argument.
More concisely: For integers `a` and natural numbers `b₁` and `b₂` with `gcd(b₁, b₂) = 1`, the Jacobi symbol `jacobiSym a (b₁ * b₂)` equals the product `jacobiSym a b₁ * jacobiSym a b₂`.
|