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 (s.prod fun (x : α) => f x) = s.prod fun (x : α) => star (f x)

@[simp]

theorem star_sum {R : Type u_1} [AddCommMonoid R] [StarAddMonoid R] {α : Type u_2} (s : Finset α) (f : α → R) : star (s.sum fun (x : α) => f x) = s.sum fun (x : α) => star (f x)