English
A product of a list of homogeneous elements is zero if each element is zero in a prefix-wise fashion.
Русский
Произведение списка однородных элементов равно нулю, если каждый элемент равен нулю на префиксах.
LaTeX
$$listProd_apply_eq_zero' ...$$
Lean4
/-- The difference with `DirectSum.multisetProd_apply_eq_zero` is that the indices at which
the terms of the multiset are zero is allowed to vary. -/
theorem multisetProd_apply_eq_zero' {s : Multiset ((⨁ i, A i) × ι)} (hs : ∀ xn ∈ s, ∀ k < xn.2, xn.1 k = 0) ⦃n : ι⦄
(hn : n < (s.map Prod.snd).sum) : (s.map Prod.fst).prod n = 0 :=
by
have :=
listProd_apply_eq_zero' (l := s.toList) (by simpa using hs) (by simpa [← Multiset.sum_coe, ← Multiset.map_coe])
simpa [← Multiset.prod_coe, ← Multiset.map_coe]
