Documentation

Mathlib.Data.Complex.BigOperators

Finite sums and products of complex numbers #

@[simp]
theorem Complex.ofReal_prod {α : Type u_1} (s : Finset α) (f : α) :
(∏ is, f i) = is, (f i)
@[simp]
theorem Complex.ofReal_sum {α : Type u_1} (s : Finset α) (f : α) :
(∑ is, f i) = is, (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 : α) :
@[simp]
theorem Complex.re_sum {α : Type u_1} (s : Finset α) (f : α) :
(∑ is, f i).re = is, (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 : α) :
@[simp]
theorem Complex.im_sum {α : Type u_1} (s : Finset α) (f : α) :
(∑ is, f i).im = is, (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 : α) :