Commit 2022-06-26 19:48 33112c45
View on Github →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