Big-operators lemmas about star algebraic operations #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
These results are kept separate from algebra.star.basic to avoid it needing to import finset.
@[simp]
theorem
star_prod
{R : Type u_1}
[comm_monoid R]
[star_semigroup R]
{α : Type u_2}
(s : finset α)
(f : α → R) :
has_star.star (s.prod (λ (x : α), f x)) = s.prod (λ (x : α), has_star.star (f x))
@[simp]
theorem
star_sum
{R : Type u_1}
[add_comm_monoid R]
[star_add_monoid R]
{α : Type u_2}
(s : finset α)
(f : α → R) :
has_star.star (s.sum (λ (x : α), f x)) = s.sum (λ (x : α), has_star.star (f x))