mathlib

33112c45 - feat(data/nat/totient): more general multiplicativity lemmas for totient (#14842)

feat(data/nat/totient): more general multiplicativity lemmas for totient (#14842) Adds lemmas: `totient_gcd_mul_totient_mul : φ (a.gcd b) * φ (a * b) = φ a * φ b * (a.gcd b)` `totient_super_multiplicative : φ a * φ b ≤ φ (a * b)` `totient_gcd_mul_totient_mul` is Theorem 2.5(b) in Apostol (1976) Introduction to Analytic Number Theory. Developed while reviewing @CBirkbeck 's #14828