op_sum — Mathlib

English

Moving to the opposite additive commutative monoid commutes with summation: op(∑_{x∈s} f(x)) = ∑_{x∈s} op(f(x)).

Русский

Перенос в противоположный аддитивный мономодийный элемент коммутирует с суммированием: op(сумма) = сумма для противоположных элементов.

LaTeX

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

Lean4

/-- Moving to the opposite additive commutative monoid commutes with summing. -/
@[simp]
theorem op_sum [AddCommMonoid M] {s : Finset ι} (f : ι → M) : op (∑ x ∈ s, f x) = ∑ x ∈ s, op (f x) :=
  map_sum (opAddEquiv : M ≃+ Mᵐᵒᵖ) _ _

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