prod_map_neg — Mathlib

English

For any list of elements in aMonoid with DistribNeg, the product of the list after applying Neg.neg equals (-1)^{length} times the original product.

Русский

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

LaTeX

$$$\bigl(\mathrm{List}.map(-1)\bigr).prod = (-1)^{|l|} \cdot l.prod$$$

Lean4

@[simp]
theorem prod_map_neg (l : List M) : (l.map Neg.neg).prod = (-1) ^ l.length * l.prod := by
  induction l <;> simp [*, pow_succ, ((Commute.neg_one_left _).pow_left _).left_comm]

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