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.ofReal_balance {α : Type u_1} [Fintype α] (f : α → ℝ) (a : α) : ↑(Fintype.balance f a) = Fintype.balance (ofReal ∘ f) a

@[simp]

theorem Complex.ofReal_comp_balance {ι : Type u_2} [Fintype ι] (f : ι → ℝ) : ofReal ∘ Fintype.balance f = Fintype.balance (ofReal ∘ f)

@[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.re_balance {α : Type u_1} [Fintype α] (f : α → ℂ) (a : α) : (Fintype.balance f a).re = Fintype.balance (re ∘ f) a

@[simp]

theorem Complex.re_comp_balance {ι : Type u_2} [Fintype ι] (f : ι → ℂ) : re ∘ Fintype.balance f = Fintype.balance (re ∘ f)

@[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

@[simp]

theorem Complex.im_balance {α : Type u_1} [Fintype α] (f : α → ℂ) (a : α) : (Fintype.balance f a).im = Fintype.balance (im ∘ f) a

@[simp]

theorem Complex.im_comp_balance {ι : Type u_2} [Fintype ι] (f : ι → ℂ) : im ∘ Fintype.balance f = Fintype.balance (im ∘ f)