Finite sums and products of complex numbers

@[simp]

theorem Complex.ofReal_prod {α : Type u_1} (s : Finset α) (f : α → ℝ) : ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)

@[simp]

theorem Complex.ofReal_sum {α : Type u_1} (s : Finset α) (f : α → ℝ) : ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)

@[simp]

theorem Complex.ofReal_expect {α : Type u_1} (s : Finset α) (f : α → ℝ) : ↑(s.expect fun (i : α) => f i) = s.expect fun (i : α) => ↑(f i)

@[simp]

theorem Complex.re_sum {α : Type u_1} (s : Finset α) (f : α → ℂ) : (∑ i ∈ s, f i).re = ∑ i ∈ s, (f i).re

@[simp]

theorem Complex.re_expect {α : Type u_1} (s : Finset α) (f : α → ℂ) : (s.expect fun (i : α) => f i).re = s.expect fun (i : α) => (f i).re

@[simp]

theorem Complex.im_sum {α : Type u_1} (s : Finset α) (f : α → ℂ) : (∑ i ∈ s, f i).im = ∑ i ∈ s, (f i).im

@[simp]

theorem Complex.im_expect {α : Type u_1} (s : Finset α) (f : α → ℂ) : (s.expect fun (i : α) => f i).im = s.expect fun (i : α) => (f i).im