In this article we formalize several basic theorems that correspond to Pell’s equation. We focus on two aspects: that the Pell’s equation x2 − Dy2 = 1 has infinitely many solutions in positive integers for a given D not being a perfect square, and that based on the least fundamental solution of the equation when we can simply calculate algebraically each remaining solution. “Solutions to Pell’s Equation” are listed as item #39 from the “Formalizing 100 Theorems” list maintained by Freek Wiedijk at http://www.cs.ru.nl/F.Wiedijk/100/.
@article{bwmeta1.element.doi-10_1515_forma-2017-0019,
author = {Marcin Acewicz and Karol P\k ak},
title = {Pell's Equation},
journal = {Formalized Mathematics},
volume = {25},
year = {2017},
pages = {197-204},
language = {en},
url = {http://dml.mathdoc.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0019}
}
Marcin Acewicz; Karol Pąk. Pell’s Equation. Formalized Mathematics, Tome 25 (2017) pp. 197-204. http://gdmltest.u-ga.fr/item/bwmeta1.element.doi-10_1515_forma-2017-0019/