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