unop_sum — Mathlib

English

Unop commutes with sum on the opposite side: unop(∑_{x∈s} f(x)) = ∑_{x∈s} unop(f(x)) for f: ι → Mᵐᵒᵖ.

Русский

Разворот несет сумму: unop(сумма) = сумма развернутых элементов.

LaTeX

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

Lean4

@[simp]
theorem unop_sum [AddCommMonoid M] {s : Finset ι} (f : ι → Mᵐᵒᵖ) : unop (∑ x ∈ s, f x) = ∑ x ∈ s, unop (f x) :=
  map_sum (opAddEquiv : M ≃+ Mᵐᵒᵖ).symm _ _

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