Journal of Formalized Reasoning (Dec 2008)
Affiliations
Read online
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.