Documentation

Mathlib.Algebra.Star.BigOperators

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)