Commit 2025-12-11 22:12 aa417d24

feat(NumberTheory/ArithmeticFunction/Carmichael): Carmichael totient function (#32414) Define ArithmeticFunction.Carmichael, the Carmichael function λ, also known as the reduced totient function. Prove the known formula for λ n in terms of the prime factorization of n, along with some useful properties:

• a ^ λ n = 1
• λ n ∣ φ n
• a ∣ b → λ a ∣ λ b
• λ (lcm a b) = lcm (λ a) (λ b)