English
For any function f from a group to a ordered star-ring, the nonnegativity of conjneg f is equivalent to the nonnegativity of f.
Русский
Для любой функции f: G → R в частично упорядоченной звездокольцу conjneg сохраняет неотрицательность, то есть 0 ≤ conjneg f эквивалентно 0 ≤ f.
LaTeX
$$$$ 0 \le \operatorname{conjneg} f \iff 0 \le f $$$$
Lean4
@[simp]
theorem conjneg_nonneg : 0 ≤ conjneg f ↔ 0 ≤ f :=
(Equiv.neg _).forall_congr' <| by simp [starRingEnd_apply]