conjneg_sum

Mathlib.Algebra.Star.Conjneg

URI: https://scilib.ai/kg/mathlib#conjneg_sum

English

conjneg commutes with finite sums (sum over a finite index set).

Русский

conjneg коммутирует с конечной суммой по индексу.

LaTeX

$$$\\text{conjneg}\\left(\\sum_{i \\in s} f(i)\\right) = \\sum_{i \\in s} \\text{conjneg}(f(i))$$$

Lean4

@[simp]
theorem conjneg_sum (s : Finset ι) (f : ι → G → R) : conjneg (∑ i ∈ s, f i) = ∑ i ∈ s, conjneg (f i) := by ext; simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru