Carmichael's totient function conjecture

Exercise · carchimichealTotientFor_zero

$n = 0 ↔ φ(n) = 0$

Formal statement · Lean 4.lean

theorem carchimichealTotientFor_zero : ¬ CarmichaelTotientFor 0 := by
  sorry

Proof. sorry

Nobody has tried yet.