prod_ne_zero_iff — Mathlib

English

A nonzero-iff criterion: f.prod g ≠ 0 iff every nonzero factor g(i, f(i)) ≠ 0 for i ∈ supp(f).

Русский

Условие неотрицательности произведения: f.prod g ≠ 0 тогда и только тогда, когда каждый не нулевой множитель g(i, f(i)) ≠ 0 для i ∈ supp(f).

LaTeX

$$$$ f.prod g \\neq 0 \\iff \\forall i \\in \\mathrm{supp}(f),\\ 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

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