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}
[inst : CommMonoid R]
[inst : StarSemigroup 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}
[inst : AddCommMonoid R]
[inst : 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)