A Page in Number Theory

Andrea Asperti, Cristian Armentano

Abstract


We discuss the formalization, in the Matita Interactive Theorem Prover, of a few elementary results in number theory about the Moebius mu function and the Euler phi function.

Full Text:

PDF (English)


DOI: 10.6092/issn.1972-5787/385

Copyright (c) 2008 Andrea Asperti, Cristian Armentano

Creative Commons License
This work is licensed under a Creative Commons Attribution 3.0 Unported License.