sum_conjneg

Mathlib.Algebra.Star.Conjneg

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

English

For a finite domain G, the sum of conjneg f over G equals the sum of conj (f a) over G.

Русский

Для конечного множества G сумма conjneg f по G равна сумме conj(f(a)) по G.

LaTeX

$$$\sum_{a \in G} \operatorname{conjneg} f(a) = \sum_{a \in G} \operatorname{conj}(f(a))$$$

Lean4

theorem sum_conjneg [Fintype G] (f : G → R) : ∑ a, conjneg f a = ∑ a, conj (f a) :=
  Fintype.sum_equiv (Equiv.neg _) _ _ fun _ ↦ rfl

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

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

Разделы

Аффилиация

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