Documentation

FormalConjectures.Wikipedia.CongruentNumber

Congruent Number #

A natural number $n$ is called a congruent number if there exists a right triangle with rational sides $a$, $b$, and hypotenuse $c$ such that the area of the triangle is $\frac{1}{2}ab = n$.

References:

def CongruentNumber.congruentNumber (n : ℕ) :

Equations

CongruentNumber.congruentNumber n = ∃ (a : ℚ) (b : ℚ) (c : ℚ), a ^ 2 + b ^ 2 = c ^ 2 ∧ ↑n = 2⁻¹ * a * b

Instances For

theorem CongruentNumber.not_congruentNumber_1 :

¬congruentNumber 1

theorem CongruentNumber.congruentNumber_5 :

congruentNumber 5

theorem CongruentNumber.congruentNumber_6 :

congruentNumber 6

theorem CongruentNumber.congruentNumber_7 :

congruentNumber 7

theorem CongruentNumber.congruentNumber_157_zagier :

congruentNumber 157

def CongruentNumber.A (n : ℕ) :

Set (ℤ × ℤ × ℤ)

Equations

CongruentNumber.A n = {(x, y, z) : ℤ × ℤ × ℤ | ↑n = 2 * x ^ 2 + y ^ 2 + 32 * z ^ 2}

Instances For

def CongruentNumber.B (n : ℕ) :

Set (ℤ × ℤ × ℤ)

Equations

CongruentNumber.B n = {(x, y, z) : ℤ × ℤ × ℤ | ↑n = 2 * x ^ 2 + y ^ 2 + 8 * z ^ 2}

Instances For

def CongruentNumber.C (n : ℕ) :

Set (ℤ × ℤ × ℤ)

Equations

CongruentNumber.C n = {(x, y, z) : ℤ × ℤ × ℤ | ↑n = 8 * x ^ 2 + 2 * y ^ 2 + 64 * z ^ 2}

Instances For

def CongruentNumber.D (n : ℕ) :

Set (ℤ × ℤ × ℤ)

Equations

CongruentNumber.D n = {(x, y, z) : ℤ × ℤ × ℤ | ↑n = 8 * x ^ 2 + 2 * y ^ 2 + 16 * z ^ 2}

Instances For

theorem CongruentNumber.Tunnell_odd (n : ℕ) (hsqf : Squarefree n) (hodd : Odd n) :

congruentNumber n → 2 * (A n).ncard = (B n).ncard

theorem CongruentNumber.Tunnell_even (n : ℕ) (hsqf : Squarefree n) (heven : Even n) :

congruentNumber n → 2 * (C n).ncard = (D n).ncard

theorem CongruentNumber.Tunnell_odd_converse (n : ℕ) (hsqf : Squarefree n) (hodd : Odd n) :

2 * (A n).ncard = (B n).ncard → congruentNumber n

theorem CongruentNumber.Tunnell_even_converse (n : ℕ) (hsqf : Squarefree n) (heven : Even n) :

2 * (C n).ncard = (D n).ncard → congruentNumber n