prod_map_neg — Mathlib

English

For a multiset s in a commutative monoid with distributive negation, the product of negated elements equals (−1)^{card s} times the product of the original elements.

Русский

Для мультимножества s в коммутативном моноиде с распределяющимся отрицанием, произведение отрицаний равно (−1)^{card s} умноженное на исходное произведение.

LaTeX

$$$\\operatorname{prod}(\\mathrm{map}(-\\mathrm{neg})\, s) = (-1)^{|s|} \\; \\operatorname{prod}(s)$$$

Lean4

@[simp]
theorem prod_map_neg (s : Multiset M) : (s.map Neg.neg).prod = (-1) ^ card s * s.prod :=
  Quotient.inductionOn s (by simp)

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