multisetProd_apply_eq_zero — Mathlib

English

The product over a multiset of homogeneous components vanishes at index n provided the corresponding prefix conditions hold for all elements.

Русский

Произведение по мультисету однородных компонент обращается в ноль на индекс n при выполнении соответствующих префиксных условий.

LaTeX

$$multisetProd_apply_eq_zero …$$

Lean4

theorem multisetProd_apply_eq_zero {s : Multiset (⨁ i, A i)} {m : ι} (hs : ∀ x ∈ s, ∀ k < m, x k = 0) ⦃n : ι⦄
    (hn : n < s.card • m) : s.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]

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