mathlib3

6089f08a - feat(data/nat/totient): add Euler's product formula for totient function (#11332)

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⁻¹)`