Euler_Phi_Function_is_Even_for_Argument_greater_than_2
Provedeuler-phi-functionnumber-theoryproofwiki
Let n >= 1. Then phi(n) is even iff n > 2.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Data.Nat.Totient
Formal statement
theorem Euler_Phi_Function_is_Even_for_Argument_greater_than_2 (n : ℕ) (hn : n > 2) : Even (Nat.totient n) := by sorry
Source