prod_ne_zero_iff — Mathlib

English

The product is nonzero iff every factor corresponding to the support is nonzero.

Русский

Произведение ненулевое тогда и только тогда, когда каждый соответствующий фактор на поддержке ненулевой.

LaTeX

$$$f.prod g \\neq 0 \\iff \\forall i \\in f.support, g i (f i) \\neq 0$$$

Lean4

theorem prod_ne_zero_iff : f.prod g ≠ 0 ↔ ∀ i ∈ f.support, g i (f i) ≠ 0 :=
  Finset.prod_ne_zero_iff

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