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