mathlib3 documentation

algebra.star.big_operators

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))