Nat.Prime.sum_four_squares
theorem Nat.Prime.sum_four_squares : ∀ {p : ℕ}, p.Prime → ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
The theorem `Nat.Prime.sum_four_squares` is known as Lagrange's Four Squares theorem for a prime number. It asserts that for any prime number `p`, there exist four natural numbers `a`, `b`, `c`, and `d` such that the sum of their squares equals `p` i.e., `a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p`. In other words, every prime number can be expressed as the sum of four square numbers. The function `Nat.sum_four_squares` should be used for practical computations.
More concisely: Every prime number can be expressed as the sum of the squares of four natural numbers.
|
Nat.euler_four_squares
theorem Nat.euler_four_squares :
∀ (a b c d x y z w : ℕ),
(↑a * ↑x - ↑b * ↑y - ↑c * ↑z - ↑d * ↑w).natAbs ^ 2 + (↑a * ↑y + ↑b * ↑x + ↑c * ↑w - ↑d * ↑z).natAbs ^ 2 +
(↑a * ↑z - ↑b * ↑w + ↑c * ↑x + ↑d * ↑y).natAbs ^ 2 +
(↑a * ↑w + ↑b * ↑z - ↑c * ↑y + ↑d * ↑x).natAbs ^ 2 =
(a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)
This is a natural number version of Euler's four-square identity. The theorem states that for any eight natural numbers (a, b, c, d, x, y, z, w), the sum of squares of four specific expressions which involve these natural numbers, each taken to the power of two, is equal to the product of the sum of squares of (a, b, c, d) and the sum of squares of (x, y, z, w). These four expressions are: the absolute value of (a*x - b*y - c*z - d*w), the absolute value of (a*y + b*x + c*w - d*z), the absolute value of (a*z - b*w + c*x + d*y), and the absolute value of (a*w + b*z - c*y + d*x).
More concisely: For any natural numbers a, b, c, d, x, y, z, w, the sum of the squares of the four expressions axBx - bயcZd - cwd - dw, aYx + bXa + cWz - dZx, aZx - bWy + cXd + dY, and aWy + bZx - cYx + dX is equal to the product of the sum of the squares of axbx, bya By, cZcZ, and dwd.
|
euler_four_squares
theorem euler_four_squares :
∀ {R : Type u_1} [inst : CommRing R] (a b c d x y z w : R),
(a * x - b * y - c * z - d * w) ^ 2 + (a * y + b * x + c * w - d * z) ^ 2 + (a * z - b * w + c * x + d * y) ^ 2 +
(a * w + b * z - c * y + d * x) ^ 2 =
(a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) * (x ^ 2 + y ^ 2 + z ^ 2 + w ^ 2)
Euler's four-square identity states that for any commutative ring R and any elements a, b, c, d, x, y, z, w of R, the sum of the squares of four specific combinations of these elements equals the product of the sum of the squares of the first four elements (a, b, c, d) and the sum of the squares of the last four elements (x, y, z, w). The specific combinations involve different multiplications, additions, and subtractions of the eight elements.
More concisely: For any commutative ring R and elements a, b, c, d, x, y, z, w, the following equality holds: (a^2 + b^2 + c^2 + d^2) * (x^2 + y^2 + z^2 + w^2) = (a^2 + b^2 + (c + d)^2) * (x^2 + y^2 + (z + w)^2)
Or, in more concise form:
(∑(a, b, c, d)^2) * (∑(x, y, z, w)^2) = (∑(a, b, c+d)^2) * (∑(x, y, z+w)^2)
Where ∑ represents the sum of squares of the elements inside the parentheses.
|
Nat.sum_four_squares
theorem Nat.sum_four_squares : ∀ (n : ℕ), ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n
The "Four Squares Theorem" states that for any natural number `n`, there exist four natural numbers `a`, `b`, `c`, and `d`, such that the sum of their squares equals `n`. In other words, any natural number can be expressed as the sum of four perfect squares.
More concisely: Every natural number can be expressed as the sum of four squares of natural numbers.
|