finsetProd_apply_eq_zero — Mathlib

English

The finset version of the zero product lemma for graded components.

Русский

Версия для конечного множества леммы о нулевом произведении компонент градации.

LaTeX

$$finsetProd_apply_eq_zero …$$

Lean4

theorem finsetProd_apply_eq_zero {s : Finset (⨁ i, A i)} {m : ι} (hs : ∀ x ∈ s, ∀ k < m, x k = 0) ⦃n : ι⦄
    (hn : n < s.card • m) : (∏ x ∈ s, x) n = 0 := by
  simpa using listProd_apply_eq_zero (l := s.toList) (by simpa using hs) (by simpa)

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