proposition: Lemma totient_pfactor p e : prime p -> e > 0 -> totient (p ^ e) = p.-1 * p ^ e.-1.
proof: Proof. move=> p_pr e_gt0; rewrite totientE ?expn_gt0 ?prime_gt0 //. by rewrite primesX // primes_prime // unlock /= muln1 pfactorK. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)