Theorem ArithmeticFunction.two_mul_carmichael_two_pow_of_three_le_eq_totient

Modification history

2025-12-11 22:12
Mathlib/NumberTheory/ArithmeticFunction/Carmichael.lean
feat(NumberTheory/ArithmeticFunction/Carmichael): Carmichael totient function (#32414) …
Added ArithmeticFunction.two_mul_carmichael_two_pow_of_three_le_eq_totientView on Github →