Theorem ArithmeticFunction.carmichael_two_pow_of_le_two_eq_totient

Modification history

2025-12-11 22:12

Mathlib/NumberTheory/ArithmeticFunction/Carmichael.lean

feat(NumberTheory/ArithmeticFunction/Carmichael): Carmichael totient function (#32414) …

Added ArithmeticFunction.carmichael_two_pow_of_le_two_eq_totient View on Github →