[STATEMENT]
lemma integral_cos_Z' [simp]:
  assumes "n \<in> \<int>"
  shows "integral\<^sup>L (lebesgue_on {-pi..pi}) (\<lambda>x. cos(n * x)) = (if n = 0 then 2 * pi else 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. LINT x|lebesgue_on {- pi..pi}. cos (n * x) = (if n = 0 then 2 * pi else 0)
[PROOF STEP]
by (metis assms integral_cos_Z mult_commute_abs)