finsetProd_apply_eq_zero' — Mathlib

English

The finite-set analogue of the previous result: finset product of homogeneous components vanishes under prefix conditions.

Русский

Конечный аналог предыдущего результата: произведение по конечному множеству гомогенных компонент обращается в ноль при префиксных условиях.

LaTeX

$$finsetProd_apply_eq_zero' …$$

Lean4

/-- The difference with `DirectSum.finsetProd_apply_eq_zero` is that the indices at which
the terms of the multiset are zero is allowed to vary. -/
theorem finsetProd_apply_eq_zero' {s : Finset ((⨁ i, A i) × ι)} (hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄
    (hn : n < ∑ xn ∈ s, xn.2) : (∏ xn ∈ s, xn.1) n = 0 := by
  simpa using listProd_apply_eq_zero' (l := s.toList) (by simpa using hs) (by simpa)

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