prod_eq_one — Mathlib

English

In a suitable setting, f.prod g = 0 iff there exists i in the support of f with g i (f i) = 0.

Русский

При определённых условиях f.prod g = 0 тогда и только тогда, существует i в поддержке f, такое что g i (f i) = 0.

LaTeX

$$$f.prod g = 0 \\iff \\exists i \\in f.support, g i (f i) = 0$$$

Lean4

@[to_additive]
theorem prod_eq_one [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] [CommMonoid γ] {f : Π₀ i, β i}
    {h : ∀ i, β i → γ} (hyp : ∀ i, h i (f i) = 1) : f.prod h = 1 :=
  Finset.prod_eq_one fun i _ => hyp i

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