Commit 2022-02-17 21:50 6089f08a

feat(data/nat/totient): add Euler's product formula for totient function (#11332) Proving four versions of Euler's product formula for the totient function φ:

• totient_eq_prod_factorization : φ n = n.factorization.prod (λ p k, p ^ (k - 1) * (p - 1))
• totient_mul_prod_factors : φ n * ∏ p in n.factors.to_finset, p = n * ∏ p in n.factors.to_finset, (p - 1)
• totient_eq_div_factors_mul : φ n = n / (∏ p in n.factors.to_finset, p) * (∏ p in n.factors.to_finset, (p - 1))
• totient_eq_mul_prod_factors : (φ n : ℚ) = n * ∏ p in n.factors.to_finset, (1 - p⁻¹)