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
Parity lemmas
1.3
The even case
1.4
The odd case
▶
1.4.1
Exercises: from factorization to sign condition
1.4.2
Key intermediate result
1.4.3
From the \(m\)-condition to finitely many solutions
1.4.4
Uniqueness per residue class
1.4.5
Verification of known solutions
1.4.6
Combining
1.5
Main theorem
▶
1.5.1
Direct computation helpers
1.5.2
The theorem
1.6
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
Parity lemmas
1.3
The even case
1.4
The odd case
1.4.1
Exercises: from factorization to sign condition
1.4.2
Key intermediate result
1.4.3
From the \(m\)-condition to finitely many solutions
1.4.4
Uniqueness per residue class
1.4.5
Verification of known solutions
1.4.6
Combining
1.5
Main theorem
1.5.1
Direct computation helpers
1.5.2
The theorem
1.6
Additional declarations