prod_neg — Mathlib

English

In a commutative monoid with a distributive negation, the product of negatives equals (-1)^{|s|} times the product of positives.

Русский

В коммутативном моноиде с распределяемым отрицанием произведение минусов равно (-1)^{|s|} умножить на произведение исходных элементов.

LaTeX

$$$$ \\prod_{x \\in s} (-f x) = (-1)^{|s|} \\cdot \\prod_{x \\in s} f x. $$$$

Lean4

theorem prod_neg [CommMonoid M] [HasDistribNeg M] (f : ι → M) : ∏ x ∈ s, -f x = (-1) ^ #s * ∏ x ∈ s, f x := by
  simpa using (s.1.map f).prod_map_neg

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