1
The Ramanujan–Nagell Theorem
▶
1.1
Setup: the quadratic ring \(R = \mathbb {Z}[(1+\sqrt{-7})/2]\)
▶
1.1.1
\(R\) is a unique factorization domain
1.2
The even case
1.3
The odd case
▶
1.3.1
Exercises: from factorization to sign condition
1.3.2
Key intermediate result
1.3.3
From the \(m\)-condition to finitely many solutions
1.3.4
Uniqueness per residue class
1.3.5
Verification of known solutions
1.3.6
Combining
1.4
Main theorem
▶
1.4.1
Direct computation
1.4.2
The theorem
1.5
Additional declarations
Dependency graph
Ramanujan Nagell in Lean
Barinder S. Banwait
1
The Ramanujan–Nagell Theorem
1.1
Setup: the quadratic ring \(R = \mathbb {Z}[(1+\sqrt{-7})/2]\)
1.1.1
\(R\) is a unique factorization domain
1.2
The even case
1.3
The odd case
1.3.1
Exercises: from factorization to sign condition
1.3.2
Key intermediate result
1.3.3
From the \(m\)-condition to finitely many solutions
1.3.4
Uniqueness per residue class
1.3.5
Verification of known solutions
1.3.6
Combining
1.4
Main theorem
1.4.1
Direct computation
1.4.2
The theorem
1.5
Additional declarations