References

1. J. Cowles & R. Gamboa (2006): Unique factorization in ACL2: Euclidean domains. In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2006, Seattle, Washington, USA, August 15-16, 2006, pp. 21–27, doi:10.1145/1217975.1217980.
2. R. Gamboa & J. Cowles (2012): A Cantor Trio: Denumerability, the Reals, and the Real Algebraic Numbers. In: Interactive Theorem Proving - Third International Conference, ITP 2012, Princeton, NJ, USA, August 13-15, 2012. Proceedings, pp. 51–66, doi:10.1007/978-3-642-32347-8_5.
3. Mu Prime Math (2020): Proof: Every Prime has a Primitive Root. https://www.youtube.com/watch?v=kHrNBwsM3lY.
4. D. Russinoff (1992): A Mechanical Proof of Quadratic Reciprocity.. J. Autom. Reasoning 8, pp. 3–21, doi:10.1007/BF00263446.
5. J.H. Silverman (2006): A Friendly Introduction to Number Theory. Pearson education international. Pearson Prentice Hall. Available at https://books.google.com/books?id=ypE_AQAAIAAJ.
6. E. Smith (2019): Prime Fields Community Books. https://www.cs.utexas.edu/users/moore/acl2/v8-4/combined-manual/index.html?topic=PFIELD____PRIME-FIELDS.
7. E. Smith (2019): Quadratic Reciprocity Community Books. https://www.cs.utexas.edu/users/moore/acl2/manuals/latest/?topic=RTL____NUMBER-THEORY.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org