prod_ite_zero — Mathlib

English

For a finite type, the product of a_i with a mixture of 0 and f_i equals 0 unless all p(i) hold; if all p(i) hold, it equals the product of f_i.

Русский

Для конечного типа произведение a_i с условием 0/функция: если все p(i) выполняются, равно произведению f_i, иначе 0.

LaTeX

$$$\\forall {ι} {M₀} [\\mathsf{Fintype} ι] [\\mathsf{CommMonoidWithZero} M₀] (p: ι \\to \\mathsf{Prop}) [\\mathsf{DecidablePred} p] (f: ι \\to M₀),\\; \\bigl(\\prod i, \\mathrm{ite}(p(i), f(i), 0)\\bigr) = \\mathrm{ite}(\\forall i, p(i), \\prod i, f(i), 0\\bigr)$$$

Lean4

theorem prod_ite_zero : (∏ i, if p i then f i else 0) = if ∀ i, p i then ∏ i, f i else 0 := by
  simp [Finset.prod_ite_zero]

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