X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Flibrary%2Fnat%2Ftotient.ma;h=a86986a81f743efd78b0dd004e38653c0788d601;hb=aa654b256f9deca4ed5bb2b13b87e1d69377f17d;hp=03e2587a8f02b1bc17eb3f3e8d0a8f932ad5417c;hpb=21d7aa4df8d5d4bfe1073720ea4f9410e9cec879;p=helm.git diff --git a/helm/software/matita/library/nat/totient.ma b/helm/software/matita/library/nat/totient.ma index 03e2587a8..a86986a81 100644 --- a/helm/software/matita/library/nat/totient.ma +++ b/helm/software/matita/library/nat/totient.ma @@ -24,7 +24,7 @@ include "nat/iteration2.ma". phi (n) is the number of naturals i (less or equal than n) so then gcd (i,n) = 1. (so this definition considers the values i=1,2,...,n) - sigma_p doesn't work ok the value n (but the first value it works on is (pred n)) + sigma_p doesn't work on the value n (but the first value it works on is (pred n)) but works also on 0. That's not a problem, in fact - if n <> 1, gcd (n,0) <>1 and gcd (n,n) = n <> 1. - if n = 1, then Phi(n) = 1, and (totient n), as defined below, returns 1. @@ -134,4 +134,4 @@ apply (nat_case1 n) ] ] ] -qed. \ No newline at end of file +qed.