prod_ne_zero_iff — Mathlib

English

For a Finset and a function into a commutative monoid without zero divisors, the product is nonzero iff every factor is nonzero.

Русский

Для Finset и функции в коммутативный моноид без делителей нуля произведение не ноль тогда и только тогда, когда каждый фактор не равен нулю.

LaTeX

$$$\\forall {ι} {M₀} [\\mathsf{CommMonoidWithZero} M₀] [\\mathsf{Nontrivial} M₀] [\\mathsf{NoZeroDivisors} M₀] (s:\\mathsf{Finset} ι) (f: ι \\to M₀),\\; (\\prod x\\in s, f x) \\neq 0 \\iff \\forall a \\in s, f a \\neq 0$$$

Lean4

theorem prod_ne_zero_iff : ∏ x ∈ s, f x ≠ 0 ↔ ∀ a ∈ s, f a ≠ 0 :=
  by
  rw [Ne, prod_eq_zero_iff]
  push_neg; rfl

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