[isabelle] phi/totient



I just noticed something peculiar about the Euler totient function in
Isabelle ("phi" in Isabelle-2016; "totient" as of 067210a08a22 in
isabelle-dev): Everyone seems to agree that Ï(1) = 1, but in Isabelle,
"phi 1 = 0" resp. "totient 1 = 0".

Furthermore, before anyone invests more time into developing that
function, I would like to point out that I have my own version of that
function in an ongoing development on Analytic Number Theory that should
end up in the AFP eventually [1].

I've shown pretty much all the basic properties of the function and a
few not-so-basic ones. My suggestion would be to change the definition
of "totient" in HOL-Number_Theory to "totient 1 = 1" and I will then
merge the more basic facts of my development into HOL-Number_Theory.

(Also, if anyone has any plans/stakes/interests in Analytic Number
Theory in Isabelle, feel free to contact me, because at the moment I'm
not sure how to continue this development, but I don't think it's quite
ready for submission to the AFP yet either)

Manuel


[1]:
https://bitbucket.org/pruvisto/dirichlet/src/df668238de758209997b0371765ed04057b1d8df/Totient.thy




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.