Big-operators lemmas about star algebraic operations

These results are kept separate from Algebra.Star.Basic to avoid it needing to import Finset.

@[simp]

theorem star_prod {R : Type u_1} [CommMonoid R] [StarMul R] {α : Type u_2} (s : Finset α) (f : α → R) : star (∏ x ∈ s, f x) = ∏ x ∈ s, star (f x)

@[simp]

theorem star_sum {R : Type u_1} [AddCommMonoid R] [StarAddMonoid R] {α : Type u_2} (s : Finset α) (f : α → R) : star (∑ x ∈ s, f x) = ∑ x ∈ s, star (f x)

theorem isSelfAdjoint_sum {R : Type u_1} {ι : Type u_2} [AddCommMonoid R] [StarAddMonoid R] (s : Finset ι) {x : ι → R} (h : ∀ i ∈ s, IsSelfAdjoint (x i)) : IsSelfAdjoint (∑ i ∈ s, x i)

@[simp]

theorem star_finsuppSum {R : Type u_1} {ι : Type u_2} {M : Type u_3} [Zero M] [AddCommMonoid R] [StarAddMonoid R] (s : ι →₀ M) (f : ι → M → R) : star (s.sum f) = s.sum fun (i : ι) (m : M) => star f i m

@[simp]

theorem star_finsuppProd {R : Type u_1} {ι : Type u_2} {M : Type u_3} [Zero M] [CommMonoid R] [StarMul R] (s : ι →₀ M) (f : ι → M → R) : star (s.prod f) = s.prod fun (i : ι) (m : M) => star f i m