Pythagorean triples

TheoremInfinitely many primitive Pythagorean triples with sides sums of two squares#●ready to prove

There are infinitely many triples \((X, Y, Z)\) of natural numbers with \(X^2 + Y^2 = Z^2\) and \(\gcd(X, Y) = 1\) such that each of \(X\), \(Y\) and \(Z\) is a sum of two squares of positive integers.

theorem_wanted primitive_pythagorean_sides_sum_two_squares_infinite :
    Set.Infinite
      {(X, Y, Z) : ℕ × ℕ × ℕ |
        X ^ 2 + Y ^ 2 = Z ^ 2 ∧ Nat.Coprime X Y ∧
          ∃ x y p q r s : ℕ,
            0 < x ∧ 0 < y ∧ 0 < p ∧ 0 < q ∧ 0 < r ∧ 0 < s ∧
              X = x ^ 2 + y ^ 2 ∧ Y = p ^ 2 + q ^ 2 ∧
                Z = r ^ 2 + s ^ 2}

Sources

• Yangcheng Li and Yong Zhang, "Primitive Pythagorean Triangles with Sides of Certain Forms", Theorem 1.

TheoremInfinitely many primitive Pythagorean triples with a square leg#●ready to prove

There are infinitely many triples \((X, Y, Z)\) of natural numbers with \(X^2 + Y^2 = Z^2\) and \(\gcd(X, Y) = 1\) such that \(X\) and \(Z\) are each a sum of two squares of positive integers and \(Y\) is the square of a positive integer.

theorem_wanted primitive_pythagorean_sides_square_middle_infinite :
    Set.Infinite
      {(X, Y, Z) : ℕ × ℕ × ℕ |
        X ^ 2 + Y ^ 2 = Z ^ 2 ∧ Nat.Coprime X Y ∧
          ∃ x y p r s : ℕ,
            0 < x ∧ 0 < y ∧ 0 < p ∧ 0 < r ∧ 0 < s ∧
              X = x ^ 2 + y ^ 2 ∧ Y = p ^ 2 ∧ Z = r ^ 2 + s ^ 2}

Sources

• Yangcheng Li and Yong Zhang, "Primitive Pythagorean Triangles with Sides of Certain Forms", Corollary 1.

TheoremInfinitely many primitive Pythagorean triples with sides sums of two cubes#●ready to prove

There are infinitely many triples \((X, Y, Z)\) of natural numbers with \(X^2 + Y^2 = Z^2\) and \(\gcd(X, Y) = 1\) such that each of \(X\), \(Y\) and \(Z\) is a sum of two cubes of positive integers.

theorem_wanted primitive_pythagorean_sides_sum_two_cubes_infinite :
    Set.Infinite
      {(X, Y, Z) : ℕ × ℕ × ℕ |
        X ^ 2 + Y ^ 2 = Z ^ 2 ∧ Nat.Coprime X Y ∧
          ∃ x y p q r s : ℕ,
            0 < x ∧ 0 < y ∧ 0 < p ∧ 0 < q ∧ 0 < r ∧ 0 < s ∧
              X = x ^ 3 + y ^ 3 ∧ Y = p ^ 3 + q ^ 3 ∧
                Z = r ^ 3 + s ^ 3}

Sources

• Yangcheng Li and Yong Zhang, "Primitive Pythagorean Triangles with Sides of Certain Forms", Theorem 2.

TheoremInfinitely many rational right triangles with sides sums of unit fractions#●ready to prove

There are infinitely many triples \((X, Y, Z)\) of positive rational numbers with \(X^2 + Y^2 = Z^2\) such that each of \(X\), \(Y\) and \(Z\) has the form \(1/u + 1/v\) for some positive integers \(u\) and \(v\).

theorem_wanted rational_right_triangles_reciprocal_sums_infinite :
    Set.Infinite
      {(X, Y, Z) : ℚ × ℚ × ℚ |
        0 < X ∧ 0 < Y ∧ 0 < Z ∧ X ^ 2 + Y ^ 2 = Z ^ 2 ∧
          ∃ x y p q r s : ℕ,
            0 < x ∧ 0 < y ∧ 0 < p ∧ 0 < q ∧ 0 < r ∧ 0 < s ∧
              X = 1 / (x : ℚ) + 1 / (y : ℚ) ∧
                Y = 1 / (p : ℚ) + 1 / (q : ℚ) ∧
                  Z = 1 / (r : ℚ) + 1 / (s : ℚ)}

Sources

• Yangcheng Li and Yong Zhang, "Primitive Pythagorean Triangles with Sides of Certain Forms", Theorem 3.

TheoremInfinitely many rational right triangles with sides differences of unit fractions#●ready to prove

There are infinitely many triples \((X, Y, Z)\) of positive rational numbers with \(X^2 + Y^2 = Z^2\) such that each of \(X\), \(Y\) and \(Z\) has the form \(1/u - 1/v\) for some positive integers \(u\) and \(v\).

theorem_wanted rational_right_triangles_reciprocal_differences_infinite :
    Set.Infinite
      {(X, Y, Z) : ℚ × ℚ × ℚ |
        0 < X ∧ 0 < Y ∧ 0 < Z ∧ X ^ 2 + Y ^ 2 = Z ^ 2 ∧
          ∃ x y p q r s : ℕ,
            0 < x ∧ 0 < y ∧ 0 < p ∧ 0 < q ∧ 0 < r ∧ 0 < s ∧
              X = 1 / (x : ℚ) - 1 / (y : ℚ) ∧
                Y = 1 / (p : ℚ) - 1 / (q : ℚ) ∧
                  Z = 1 / (r : ℚ) - 1 / (s : ℚ)}

Sources

• Yangcheng Li and Yong Zhang, "Primitive Pythagorean Triangles with Sides of Certain Forms", Theorem 3.

DefinitionAmato's cathetus parameter set#✓fully proved

For a natural number \(x\), let \(n\) be the exponent of \(2\) in \(x\) (taken to be \(0\) for \(x = 0\)). The set \(C(x)\) consists of the natural numbers \(d\) with \(d \le x\) and \(d \mid x^2\) such that, if \(x\) is even, \(d = 2^s l\) for some natural numbers \(s\) and \(l\) with \(1 \le s \le n - 1\) and \(l \mid x^2\).

This is the definition as printed in the source: for odd \(x\) it is \(D(x) = \{d \in \mathbb{N} : d \le x,\ d \mid x^2\}\), and for even \(x = 2^n k\) with \(k\) odd it is \(D(x) \cap P(x)\) with \(P(x) = \{2^s l : l \mid x^2,\ s \in \{1, \dots, n - 1\}\}\).

def amatoCathetusParams (x : ℕ) : Set ℕ :=
  {d | d ≤ x ∧ d ∣ x ^ 2 ∧
    (Even x → ∃ s l : ℕ, 1 ≤ s ∧ s ≤ padicValNat 2 x - 1 ∧ l ∣ x ^ 2 ∧ d = 2 ^ s * l)}

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Theorem 1 (quoting [1]).

Used by 3

Used byAmato's parameter set for the cathetus \(3\) contains \(1\) · Products of Pythagorean triples through a cathetus · \(2\) is an Amato parameter for the cathetus \(4\)

TheoremAmato's parameter set for the cathetus \(3\) contains \(1\)#✓fully proved

We have \(1 \in C(3)\), where \(C(x)\) is Amato's cathetus parameter set.

The parameter \(d = 1\) generates the triple \((3, 4, 5)\).

theorem one_mem_amatoCathetusParams_three : 1 ∈ amatoCathetusParams 3

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Theorem 1 (quoting [1]).

Uses 1

Statement usesAmato's cathetus parameter set

Theorem\(2\) is an Amato parameter for the cathetus \(4\)#✓fully proved

The number \(2\) belongs to Amato's parameter set \(C(4)\) for the cathetus \(4\).

With \(x = 4\) and \(d = 2\), the formulas \(x^2 / (2d) \mp d / 2\) give \(3\) and \(5\), so \(2\) generates the triple \((4, 3, 5)\).

theorem two_mem_amatoCathetusParams_four : 2 ∈ amatoCathetusParams 4

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Theorem 1 (quoting [1]).

Uses 1

Statement usesAmato's cathetus parameter set

TheoremProducts of Pythagorean triples through a cathetus#●ready to prove

Let \(a\) and \(b\) be positive natural numbers, and let \(d_1 \in C(a)\) and \(d_2 \in C(b)\), where \(C(x)\) is Amato's cathetus parameter set. Define the rational numbers \(a_1 = a^2/(2 d_1) - d_1/2\), \(a_2 = a^2/(2 d_1) + d_1/2\), \(b_1 = b^2/(2 d_2) - d_2/2\), \(b_2 = b^2/(2 d_2) + d_2/2\), \(y = (ab)^2/(2 d_1 d_2) - d_1 d_2/2\) and \(z = (ab)^2/(2 d_1 d_2) + d_1 d_2/2\), so that \((a, a_1, a_2)\), \((b, b_1, b_2)\) and \((ab, y, z)\) are the triples generated by \(d_1\), \(d_2\) and \(d_1 d_2\) through \(x^2/(2d) \mp d/2\). Then \(y = a_1 b_2 + a_2 b_1\), \(z = a_1 b_2 + a_2 b_1 + d_1 d_2\), \(y = a_1 b_1 + a_2 b_2 - d_1 d_2\), \(z = a_1 b_1 + a_2 b_2\), and \(d_1 d_2 \in C(ab)\).

The source takes any triple \((ab, y, z)\) with \(z - y = d_3 \in C(ab)\) and concludes \(d_3 = d_1 d_2\), which is false as printed: for \((3, 4, 5)\) taken twice (\(d_1 = d_2 = 1\)) and \((9, 12, 15)\) (\(d_3 = 3 \in C(9)\)), \(d_3 \ne d_1 d_2\) and \(a_1 b_2 + a_2 b_1 = 40 \ne 12\). Following the closing clause "with \(d_3 = d_1 \cdot d_2\)", the triple for \(ab\) is the one generated by \(d_3 = d_1 d_2\).

public theorem_wanted pythagorean_cathetus_product (a b d₁ d₂ : ℕ) (ha : 0 < a) (hb : 0 < b)
    (hd₁ : d₁ ∈ amatoCathetusParams a) (hd₂ : d₂ ∈ amatoCathetusParams b) :
    let a₁ : ℚ := (a : ℚ) ^ 2 / (2 * d₁) - d₁ / 2
    let a₂ : ℚ := (a : ℚ) ^ 2 / (2 * d₁) + d₁ / 2
    let b₁ : ℚ := (b : ℚ) ^ 2 / (2 * d₂) - d₂ / 2
    let b₂ : ℚ := (b : ℚ) ^ 2 / (2 * d₂) + d₂ / 2
    let y : ℚ := ((a : ℚ) * b) ^ 2 / (2 * (d₁ * d₂)) - d₁ * d₂ / 2
    let z : ℚ := ((a : ℚ) * b) ^ 2 / (2 * (d₁ * d₂)) + d₁ * d₂ / 2
    y = a₁ * b₂ + a₂ * b₁ ∧ z = a₁ * b₂ + a₂ * b₁ + d₁ * d₂ ∧
      y = a₁ * b₁ + a₂ * b₂ - d₁ * d₂ ∧ z = a₁ * b₁ + a₂ * b₂ ∧
      d₁ * d₂ ∈ amatoCathetusParams (a * b)

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Theorem 2 (quoting [1], [3]).

Uses 1

Statement usesAmato's cathetus parameter set

DefinitionAmato's product of triples#✓fully proved

For a commutative ring \(R\), the product of two triples \((x, y, z)\) and \((x', y', z')\) in \(R^3\) is

\[(x, y, z) \star (x', y', z') = (x x',\ y z' + z y',\ y z' + z y' + (z - y)(z' - y')).\]

This is the source's product (4); its operation (12) on integral triples is the same formula.

def pythagoreanTripleMul {R : Type*} [CommRing R] (u v : R × R × R) : R × R × R :=
  (u.1 * v.1, u.2.1 * v.2.2 + u.2.2 * v.2.1,
    u.2.1 * v.2.2 + u.2.2 * v.2.1 + (u.2.2 - u.2.1) * (v.2.2 - v.2.1))

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Lemma 1, (4).

Used by 5

Used byIntegral Pythagorean triples form a commutative monoid · Amato's product preserves rational Pythagorean triples · Right identity for Amato's product · Amato's product of \((3, 4, 5)\) with itself · Group laws for Amato's product on rational Pythagorean triples

TheoremAmato's product of \((3, 4, 5)\) with itself#✓fully proved

For integer triples, \((3, 4, 5) \star (3, 4, 5) = (9, 40, 41)\), where \(\star\) is Amato's product of triples.

theorem pythagoreanTripleMul_three_four_five :
    pythagoreanTripleMul ((3, 4, 5) : ℤ × ℤ × ℤ) (3, 4, 5) = (9, 40, 41)

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Lemma 1, (4).

Uses 1

Statement usesAmato's product of triples

TheoremRight identity for Amato's product#✓fully proved

For every commutative ring \(R\) and every triple \(u \in R^3\), we have \(u \star (1, 0, 1) = u\), where \(\star\) is Amato's product of triples.

theorem pythagoreanTripleMul_one {R : Type*} [CommRing R] (u : R × R × R) :
    pythagoreanTripleMul u (1, 0, 1) = u

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Theorem 3, (7)-(8).

Uses 1

Statement usesAmato's product of triples

DefinitionRational Pythagorean triples#✓fully proved

The set \(E\) consists of the triples \((x, y, z)\) of rational numbers with \(x \ne 0\) and \(x^2 + y^2 = z^2\).

def ratPythagoreanTriples : Set (ℚ × ℚ × ℚ) :=
  {v | v.1 ≠ 0 ∧ v.1 ^ 2 + v.2.1 ^ 2 = v.2.2 ^ 2}

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Section 2, definition of E.

Used by 3

Used byAmato's product preserves rational Pythagorean triples · Group laws for Amato's product on rational Pythagorean triples · \((3, 4, 5)\) is a rational Pythagorean triple

Theorem\((3, 4, 5)\) is a rational Pythagorean triple#✓fully proved

The triple \((3, 4, 5)\) belongs to the set \(E\) of rational triples \((x, y, z)\) with \(x \neq 0\) and \(x^2 + y^2 = z^2\).

theorem three_four_five_mem_ratPythagoreanTriples :
    ((3, 4, 5) : ℚ × ℚ × ℚ) ∈ ratPythagoreanTriples

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Section 2, definition of E.

Uses 1

Statement usesRational Pythagorean triples

TheoremAmato's product preserves rational Pythagorean triples#●ready to prove

Let \(E\) be the set of rational triples \((x, y, z)\) with \(x \ne 0\) and \(x^2 + y^2 = z^2\), and let \(\star\) be Amato's product of triples. If \(u \in E\) and \(v \in E\), then \(u \star v \in E\); that is, \(\star\) is a binary operation on \(E\).

The source's fraction representation \((a/b, c/d, e/f)\) with \(a, b, d, f \ne 0\) describes the same set \(E\).

public theorem_wanted pythagoreanTripleMul_mem_ratPythagoreanTriples (u v : ℚ × ℚ × ℚ)
    (hu : u ∈ ratPythagoreanTriples) (hv : v ∈ ratPythagoreanTriples) :
    pythagoreanTripleMul u v ∈ ratPythagoreanTriples

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Lemma 1.

Uses 2

Statement usesAmato's product of triples · Rational Pythagorean triples

TheoremGroup laws for Amato's product on rational Pythagorean triples#●ready to prove

Let \(E\) be the set of rational triples \((x, y, z)\) with \(x \ne 0\) and \(x^2 + y^2 = z^2\), and let \(\star\) be Amato's product of triples. Then \((1, 0, 1) \in E\); \((u \star v) \star w = u \star (v \star w)\) for all \(u, v, w \in E\); \(u \star v = v \star u\) for all \(u, v \in E\); \(u \star (1, 0, 1) = u\) for every \(u \in E\); every \(u \in E\) has some \(v \in E\) with \(u \star v = (1, 0, 1)\); and \(E\) is infinite.

Together with the closure of \(E\) under \(\star\) (stated separately), this makes \(E\) an infinite commutative group under \(\star\) with identity \((1, 0, 1)\).

public theorem_wanted ratPythagoreanTriples_commGroup :
    ((1, 0, 1) : ℚ × ℚ × ℚ) ∈ ratPythagoreanTriples ∧
      (∀ u ∈ ratPythagoreanTriples, ∀ v ∈ ratPythagoreanTriples, ∀ w ∈ ratPythagoreanTriples,
        pythagoreanTripleMul (pythagoreanTripleMul u v) w =
          pythagoreanTripleMul u (pythagoreanTripleMul v w)) ∧
      (∀ u ∈ ratPythagoreanTriples, ∀ v ∈ ratPythagoreanTriples,
        pythagoreanTripleMul u v = pythagoreanTripleMul v u) ∧
      (∀ u ∈ ratPythagoreanTriples, pythagoreanTripleMul u (1, 0, 1) = u) ∧
      (∀ u ∈ ratPythagoreanTriples, ∃ v ∈ ratPythagoreanTriples,
        pythagoreanTripleMul u v = (1, 0, 1)) ∧
      ratPythagoreanTriples.Infinite

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Theorem 3.

Uses 2

Statement usesAmato's product of triples · Rational Pythagorean triples

TheoremIntegral Pythagorean triples form a commutative monoid#●ready to prove

Let \(M\) be the set of integer triples \((a, b, c)\) with \(a^2 + b^2 = c^2\), let \(N\) be the set of triples in \(M\) whose three entries are nonnegative, and let \(\star\) be Amato's product of triples. Then the product of two triples in \(M\) lies in \(M\), \(\star\) is associative and commutative on \(M\), and \(u \star (1, 0, 1) = u\) for every \(u \in M\). Moreover \((1, 0, 1) \in N\), the product of two triples in \(N\) lies in \(N\), and \(N\) is infinite. So \(M\) is an infinite commutative monoid with identity \((1, 0, 1)\), and \(N\) is an infinite submonoid.

The source prints its operation (12) as \((a, b, c) \star (e, f, g) = (ae, bf + ce, \dots)\) with \(d_2 = f - e\); it is read as \((a, b, c) \star (d, e, f) = (ad,\ bf + ce,\ bf + ce + (c - b)(f - e))\), the integral case of (4), as the source states.

public theorem_wanted intPythagoreanTriples_commMonoid :
    let M : Set (ℤ × ℤ × ℤ) := {v | v.1 ^ 2 + v.2.1 ^ 2 = v.2.2 ^ 2}
    let N : Set (ℤ × ℤ × ℤ) := {v | v ∈ M ∧ 0 ≤ v.1 ∧ 0 ≤ v.2.1 ∧ 0 ≤ v.2.2}
    (1, 0, 1) ∈ N ∧
      (∀ u ∈ M, ∀ v ∈ M, pythagoreanTripleMul u v ∈ M) ∧
      (∀ u ∈ N, ∀ v ∈ N, pythagoreanTripleMul u v ∈ N) ∧
      (∀ u ∈ M, ∀ v ∈ M, ∀ w ∈ M, pythagoreanTripleMul (pythagoreanTripleMul u v) w =
        pythagoreanTripleMul u (pythagoreanTripleMul v w)) ∧
      (∀ u ∈ M, ∀ v ∈ M, pythagoreanTripleMul u v = pythagoreanTripleMul v u) ∧
      (∀ u ∈ M, pythagoreanTripleMul u (1, 0, 1) = u) ∧
      N.Infinite

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Corollary 1.

Uses 1

Statement usesAmato's product of triples

DefinitionAmato's product on rational points of the unit circle#✓fully proved

For rational pairs \((x, y)\) and \((x', y')\), the product is \((x, y) \odot (x', y') = (x x' / (1 + y y'), (y + y') / (1 + y y'))\), where division by \(0\) gives \(0\); so the product is \((0, 0)\) when \(1 + y y' = 0\).

For points \((a/c, b/c)\) and \((d/f, e/f)\) with \(c, f \neq 0\) this reads \((ad / (cf + eb), (bf + ec) / (cf + eb))\), the form (14)(I) of the source.

def unitCircleRatMul (p q : ℚ × ℚ) : ℚ × ℚ :=
  (p.1 * q.1 / (1 + p.2 * q.2), (p.2 + q.2) / (1 + p.2 * q.2))

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Theorem 4, (14)(I).

Used by 2

Used byAmato's group law on rational points of the unit circle · Squaring \((3/5, 4/5)\) under Amato's product

TheoremSquaring \((3/5, 4/5)\) under Amato's product#✓fully proved

For Amato's product \((x, y) \odot (x', y') = (x x' / (1 + y y'), (y + y') / (1 + y y'))\) on \(\mathbb{Q}^2\), we have \((3/5, 4/5) \odot (3/5, 4/5) = (9/41, 40/41)\).

theorem unitCircleRatMul_three_four_five :
    unitCircleRatMul (3 / 5, 4 / 5) (3 / 5, 4 / 5) = (9 / 41, 40 / 41)

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Theorem 4, (14)(I).

Uses 1

Statement usesAmato's product on rational points of the unit circle

TheoremAmato's group law on rational points of the unit circle#●ready to prove

Let \(P = \{(x, y) \in \mathbb{Q}^2 : x \neq 0,\ x^2 + y^2 = 1\}\) and let \(\odot\) be Amato's product \((x, y) \odot (x', y') = (x x' / (1 + y y'), (y + y') / (1 + y y'))\). Then \((1, 0) \in P\); for all \(p, q \in P\) we have \(p \odot q \in P\); \(\odot\) is associative and commutative on \(P\); for every \((x, y) \in P\) we have \((x, y) \odot (1, 0) = (x, y)\) and \((x, y) \odot (x, -y) = (1, 0)\); and \(P\) is infinite.

\(P\) is the set of points \((a/c, b/c)\) coming from primitive Pythagorean triples \((a, b, c)\) with \(a \neq 0\): writing a rational point of the unit circle over its reduced common denominator gives a primitive triple. Rules (II) and (III) of (14) in the source concern fraction representatives and hold automatically in \(\mathbb{Q}\).

public theorem_wanted unitCircleRat_commGroup :
    let P : Set (ℚ × ℚ) := {p | p.1 ≠ 0 ∧ p.1 ^ 2 + p.2 ^ 2 = 1}
    (1, 0) ∈ P ∧
      (∀ p ∈ P, ∀ q ∈ P, unitCircleRatMul p q ∈ P) ∧
      (∀ p ∈ P, ∀ q ∈ P, ∀ r ∈ P,
        unitCircleRatMul (unitCircleRatMul p q) r = unitCircleRatMul p (unitCircleRatMul q r)) ∧
      (∀ p ∈ P, ∀ q ∈ P, unitCircleRatMul p q = unitCircleRatMul q p) ∧
      (∀ p ∈ P, unitCircleRatMul p (1, 0) = p) ∧
      (∀ p ∈ P, unitCircleRatMul p (p.1, -p.2) = (1, 0)) ∧
      P.Infinite

Sources

• Roberto Amato, Groups and Monoid in the Set of Pythagorean Triples, INTEGERS 24 (2024), Article A5, Theorem 4.

Uses 1

Statement usesAmato's product on rational points of the unit circle

10 fully proved10 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.