tprod_comp_neg — Mathlib

English

If f: β → α and β carries an involutive negation, then ∏' d, f(-d) = ∏' d, f(d).

Русский

Если есть инволютивное отрицание на β, тогда т-произведение по d и f(-d) равно т-произведению по d и f(d).

LaTeX

$$$\\\\prod' d, f(-d) = \\\\prod' d, f(d)$$$

Lean4

@[to_additive (attr := simp)]
theorem tprod_comp_neg {β : Type*} [InvolutiveNeg β] (f : β → α) : ∏' d, f (-d) = ∏' d, f d :=
  (Equiv.neg β).tprod_eq f

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