totient): add totient_mul_prime_div (#10971)

Commit

3 years ago

feat(data/nat/totient): add totient_mul_prime_div (#10971) We add `(p * n).totient = p * n.totient` if `p ∣ n`.

Author

riccardobrasca

Parents