1
The Ramanujan–Nagell Theorem
▶
1.1
Setup: the ring of integers of \(\mathbb {Q}(\sqrt{-7})\)
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 ring of integers of \(\mathbb {Q}(\sqrt{-7})\)
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