prod_eq_zero — Mathlib

English

The product over i of f(i) is zero iff there exists an index i with f(i) = 0.

Русский

Произведение по i от f(i) равно нулю тогда и только тогда, когда существует i, для которого f(i) = 0.

LaTeX

$$$ \prod_{i: \iota} f(i) = 0 \;\Leftrightarrow\; \exists i, f(i) = 0 $$$

Lean4

@[simp]
theorem prod_eq_zero {ι} (f : ι → Cardinal.{u}) : prod f = 0 ↔ ∃ i, f i = 0 :=
  by
  lift f to ι → Type u using fun _ => trivial
  simp only [mk_eq_zero_iff, ← mk_pi, isEmpty_pi]

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