theorem CarmichaelTotient.carmichael_totient_conjecture (n : ℕ) : ¬HasUniquePositiveTotientPreimage n

Carmichael's totient conjecture: no natural number has exactly one positive preimage under Euler's totient function.