Module docstring
{"# Big-operators lemmas about star algebraic operations
These results are kept separate from Algebra.Star.Basic to avoid it needing to import Finset.
"}
star_prod
theorem
[CommMonoid R] [StarMul R] {α : Type*} (s : Finset α) (f : α → R) : star (∏ x ∈ s, f x) = ∏ x ∈ s, star (f x)
Full source
@[simp]
theorem star_prod [CommMonoid R] [StarMul R] {α : Type*} (s : Finset α) (f : α → R) :
star (∏ x ∈ s, f x) = ∏ x ∈ s, star (f x) := map_prod (starMulAut : R ≃* R) _ _Informal description
Let $R$ be a commutative monoid equipped with a star operation satisfying the *-magma property. For any finite set $s$ and any function $f \colon s \to R$, the star of the product $\prod_{x \in s} f(x)$ is equal to the product of the stars $\prod_{x \in s} \star(f(x))$. In symbols:
\[ \star\left( \prod_{x \in s} f(x) \right) = \prod_{x \in s} \star(f(x)). \]
star_sum
theorem
[AddCommMonoid R] [StarAddMonoid R] {α : Type*} (s : Finset α) (f : α → R) : star (∑ x ∈ s, f x) = ∑ x ∈ s, star (f x)
Full source
@[simp]
theorem star_sum [AddCommMonoid R] [StarAddMonoid R] {α : Type*} (s : Finset α) (f : α → R) :
star (∑ x ∈ s, f x) = ∑ x ∈ s, star (f x) := map_sum (starAddEquiv : R ≃+ R) _ _Informal description
Let $R$ be an additive commutative monoid equipped with a star operation that is involutive and preserves addition. For any finite set $s$ and any function $f \colon \alpha \to R$, the star of the sum of $f$ over $s$ is equal to the sum of the star of $f$ over $s$, i.e.,
\[
\star \left( \sum_{x \in s} f(x) \right) = \sum_{x \in s} \star(f(x)).
\]