finprod_eq_zero — Mathlib

English

If some f(x) = 0 and the mulSupport is finite, then the finprod is 0.

Русский

Если некоторое f(x) = 0 и mulSupport конечен, то финпроизведение равно 0.

LaTeX

$$$\\exists x, f(x)=0 \\Rightarrow \\ prod^\\!x, f(x) = 0$$$

Lean4

theorem finprod_eq_zero {M₀ : Type*} [CommMonoidWithZero M₀] (f : α → M₀) (x : α) (hx : f x = 0)
    (hf : (mulSupport f).Finite) : ∏ᶠ x, f x = 0 := by
  nontriviality
  rw [finprod_eq_prod f hf]
  refine Finset.prod_eq_zero (hf.mem_toFinset.2 ?_) hx
  simp [hx]

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