star_sum — Mathlib

English

The star operation distributes over finite sums in a star-ordered additive setting.

Русский

Операция star распространяется на сумму по конечному числу слагаемых в аддитивной структуре с star.

LaTeX

$$$\\star\\left(\\sum_{x \\in s} f(x)\\right) = \\sum_{x \\in s} \\star(f(x)).$$$

Lean4

@[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) _ _

Похожие утверждения