ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime
theorem ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime :
∀ {n x y : ℤ}, n = x ^ 2 + y ^ 2 → IsCoprime x y → IsSquare (-1)
This theorem states that if an integer `n` can be represented as the sum of two squares of coprime integers `x` and `y` (i.e., `n = x^2 + y^2` where `x` and `y` are coprime), then `-1` is a square in the ring of integers modulo `n`. That is, there exists an integer `r` such that `-1` is congruent to `r^2` modulo `n`. The notion of being coprime is defined here as the existence of integers `a` and `b` such that `a * x + b * y = 1`, and an element `a` is considered a square if there exists `r` such that `a = r * r`.
More concisely: If an integer `n` can be expressed as the sum of two coprime squares (i.e., `n = x^2 + y^2` with `x` and `y` coprime), then `-1` is a quadratic residue modulo `n`, i.e., there exists an integer `r` such that `r^2 ≡ -1 (mod n)`.
|
sq_add_sq_mul
theorem sq_add_sq_mul :
∀ {R : Type u_1} [inst : CommRing R] {a b x y u v : R},
a = x ^ 2 + y ^ 2 → b = u ^ 2 + v ^ 2 → ∃ r s, a * b = r ^ 2 + s ^ 2
This theorem states that in any commutative ring, the set of sums of two squares is closed under multiplication. More precisely, given any elements `x`, `y`, `u`, `v` in a commutative ring `R`, if `a` equals the sum of the squares of `x` and `y`, and `b` equals the sum of the squares of `u` and `v`, then the product of `a` and `b` is also the sum of squares of two elements `r` and `s` in the ring.
More concisely: In a commutative ring, the product of two sums of squares is a sum of squares.
|
Nat.sq_add_sq_mul
theorem Nat.sq_add_sq_mul : ∀ {a b x y u v : ℕ}, a = x ^ 2 + y ^ 2 → b = u ^ 2 + v ^ 2 → ∃ r s, a * b = r ^ 2 + s ^ 2
This theorem states that for any natural numbers `a`, `b`, `x`, `y`, `u`, and `v`, if `a` equals the sum of squares of `x` and `y`, and `b` equals the sum of squares of `u` and `v`, then there exist natural numbers `r` and `s` such that the product of `a` and `b` equals the sum of squares of `r` and `s`. In other words, the set of natural numbers that can be expressed as the sum of two squares is closed under multiplication.
More concisely: If `a` is the sum of squares of two natural numbers `x` and `y`, and `b` is the sum of squares of natural numbers `u` and `v`, then there exist natural numbers `r` and `s` such that `a * b` is the sum of squares of `r` and `s`.
|
Nat.Prime.mod_four_ne_three_of_dvd_isSquare_neg_one
theorem Nat.Prime.mod_four_ne_three_of_dvd_isSquare_neg_one :
∀ {p n : ℕ}, p.Prime → p ∣ n → IsSquare (-1) → p % 4 ≠ 3
This theorem states that for any natural numbers `p` and `n`, if `p` is a prime number and `p` divides `n` such that `-1` is a square modulo `n`, then the remainder of `p` when divided by `4` cannot be `3`. In other words, any prime `p` that divides a number `n` where `-1` is a perfect square in the modulo `n` arithmetic must be of the form `4k + 1` or `4k + 2` for some natural number `k`, but can't be of the form `4k + 3`.
More concisely: A prime number `p` that divides a number `n` such that `-1` is a perfect square modulo `n` cannot be of the form `4k + 3` for any natural number `k`.
|
Nat.Prime.sq_add_sq
theorem Nat.Prime.sq_add_sq : ∀ {p : ℕ} [inst : Fact p.Prime], p % 4 ≠ 3 → ∃ a b, a ^ 2 + b ^ 2 = p
Fermat's theorem on the sum of two squares, also known as Fermat's Christmas theorem, states that for every prime number that is not congruent to 3 modulo 4, there exist two natural numbers `a` and `b` such that the sum of their squares equals the prime number. In other words, if `p` is a prime number and `p % 4 ≠ 3`, then we can find `a` and `b` such that `a ^ 2 + b ^ 2 = p`.
More concisely: For every prime number p not congruent to 3 modulo 4, there exist integers a and b such that a^2 + b^2 = p.
|
ZMod.isSquare_neg_one_iff'
theorem ZMod.isSquare_neg_one_iff' : ∀ {n : ℕ}, Squarefree n → (IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3) := by
sorry
The theorem `ZMod.isSquare_neg_one_iff'` states that for any natural number `n` which is squarefree (meaning the only perfect square numbers that divide it are the squares of the unit elements of the monoid), `-1` is a square modulo `n` if and only if there is no divisor `q` of `n` that is equivalent to 3 modulo 4. In other words, if `n` is a squarefree number, then `-1` being a perfect square in the modular arithmetic of `n` is equivalent to the assertion that none of the divisors of `n` gives a remainder of 3 when divided by 4.
More concisely: For a squarefree natural number `n`, `-1` is a square modulo `n` if and only if there is no divisor of `n` congruent to 3 modulo 4.
|
Nat.eq_sq_add_sq_iff_eq_sq_mul
theorem Nat.eq_sq_add_sq_iff_eq_sq_mul : ∀ {n : ℕ}, (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∃ a b, n = a ^ 2 * b ∧ IsSquare (-1)
A natural number `n` is expressed as a sum of two squares if and only if `n` can be written as the product of the square of a natural number `a` and another natural number `b`, such that `-1` is a perfect square in the multiplication group modulo `b`. That is, there exists some `r` such that `(-1) = r * r (mod b)`.
More concisely: A natural number `n` is the sum of two squares if and only if there exists natural numbers `a` and `b` such that `n = a^2 * b^2` and `(-1)` is a quadratic residue modulo `b`.
|
ZMod.isSquare_neg_one_mul
theorem ZMod.isSquare_neg_one_mul : ∀ {m n : ℕ}, m.Coprime n → IsSquare (-1) → IsSquare (-1) → IsSquare (-1)
The theorem `ZMod.isSquare_neg_one_mul` states that for any two coprime natural numbers `m` and `n`, if `-1` is a square modulo `m` and `n` (meaning there exist numbers `r` and `s` such that `-1` is congruent to `r*r` modulo `m` and `s*s` modulo `n`), then `-1` is also a square modulo `m*n` (meaning there exists a number `t` such that `-1` is congruent to `t*t` modulo `m*n`).
More concisely: If `m` and `n` are coprime natural numbers and `-1` is a quadratic residue modulo both `m` and `n`, then `-1` is a quadratic residue modulo their product `m*n`.
|
ZMod.isSquare_neg_one_iff
theorem ZMod.isSquare_neg_one_iff :
∀ {n : ℕ}, Squarefree n → (IsSquare (-1) ↔ ∀ {q : ℕ}, q.Prime → q ∣ n → q % 4 ≠ 3)
The theorem `ZMod.isSquare_neg_one_iff` states that for any squarefree natural number `n`, `-1` is a square modulo `n` if and only if there is no prime `q` that divides `n` where `q` modulo 4 is equal to 3. In other words, if `n` is a squarefree number, `-1` being a perfect square in the modulus `n` system implies that no prime `q` satisfying `q % 4 = 3` can divide `n`, and vice versa. Here, a squarefree number is one which is not divisible by any perfect square, except 1 and a prime number `q` is a natural number greater than 1 whose only factors are 1 and itself.
More concisely: For a squarefree natural number $n$, $-1$ is a square modulo $n$ if and only if there is no prime $q$ dividing $n$ such that $q \equiv 3 \pmod{4}$.
|
Nat.eq_sq_add_sq_iff
theorem Nat.eq_sq_add_sq_iff :
∀ {n : ℕ}, (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ {q : ℕ}, q.Prime → q % 4 = 3 → Even (padicValNat q n)
A positive natural number `n` can be expressed as the sum of two squares if and only if for every prime number `q` in its prime factorization, where `q` modulo 4 equals 3, the `q`-adic valuation of `n` (the highest power of `q` that divides `n`) is an even number. Note that the assumption `n > 0` is not required since for `n = 0`, both conditions are automatically satisfied; the right-hand side is true because by definition `padicValNat q 0 = 0`.
More concisely: A natural number `n` can be expressed as the sum of two squares if and only if the highest power of every prime `q` in its prime factorization, where `q` is congruent to 3 modulo 4, in its prime factorization has even power.
|
ZMod.isSquare_neg_one_of_dvd
theorem ZMod.isSquare_neg_one_of_dvd : ∀ {m n : ℕ}, m ∣ n → IsSquare (-1) → IsSquare (-1)
The theorem `ZMod.isSquare_neg_one_of_dvd` states that for any two natural numbers `m` and `n`, if `m` divides `n` and `-1` is a square modulo `n` (meaning there exists a number `r` such that `r*r = -1 mod n`), then `-1` is also a square modulo `m` (i.e., there exists a number `s` such that `s*s = -1 mod m`).
More concisely: If `m` divides `n` and `-1` is a square modulo `n`, then `-1` is a square modulo `m`.
|
Nat.eq_sq_add_sq_of_isSquare_mod_neg_one
theorem Nat.eq_sq_add_sq_of_isSquare_mod_neg_one : ∀ {n : ℕ}, IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
This theorem states that for any natural number `n`, if `-1` is a square under modulo operation with `n` (i.e., `-1` can be expressed as the square of some number modulo `n`), then `n` can be expressed as the sum of squares of two natural numbers. In mathematical terms, if exists `r` such that `-1 ≡ r^2 (mod n)`, then there exist two natural numbers `x` and `y` such that `n = x^2 + y^2`.
More concisely: If `n` is a natural number such that `-1` is a quadratic residue modulo `n`, then `n` can be expressed as the sum of two squares of natural numbers.
|
ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime
theorem ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime :
∀ {n x y : ℕ}, n = x ^ 2 + y ^ 2 → x.Coprime y → IsSquare (-1)
The theorem `ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_coprime` states that for any natural numbers `n`, `x`, and `y`, if `n` is equal to the sum of the squares of `x` and `y`, and `x` and `y` are coprime, then `-1` is a square number in modulo `n`. In other words, there exists a natural number `r` such that `r * r` is congruent to `-1` modulo `n`. This theorem is useful in the field of number theory, particularly in the study of quadratic residues.
More concisely: If `n` is the sum of the squares of two coprime natural numbers `x` and `y`, then `-1` is a square modulo `n`.
|