Carmichael's totient function conjecture

Theorem · carmichealTotientFor_odd

For every odd number $n$ , $φ(2n) = φ(n)$

Formal statement · Lean 4.lean

theorem carmichealTotientFor_odd {n : ℕ} (hn : Odd n) : CarmichaelTotientFor n := by
  sorry

Proof. sorry

Nobody has tried yet.