[STATEMENT]
lemma sum_conjugate:
  fixes f :: "'b \<Rightarrow> 'a :: conjugatable_ring"
  assumes finX: "finite X"
  shows "conjugate (sum f X) = sum (\<lambda>x. conjugate (f x)) X"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. conjugate (sum f X) = (\<Sum>x\<in>X. conjugate (f x))
[PROOF STEP]
using finX
[PROOF STATE]
proof (prove)
using this:
finite X

goal (1 subgoal):
 1. conjugate (sum f X) = (\<Sum>x\<in>X. conjugate (f x))
[PROOF STEP]
by (induct set:finite, auto simp: conjugate_dist_add)