prod_eq_zero

Mathlib.Algebra.BigOperators.Ring.Multiset

URI: https://scilib.ai/kg/mathlib#Multiset.prod_eq_zero

English

In a commutative monoid with zero, if 0 is contained in a multiset s, then s.prod = 0.

Русский

В коммутативном моноиде с нулём, если 0 принадлежит мультимножество s, то s.prod = 0.

LaTeX

$$$0 \in s \Rightarrow s.prod = 0$$$

Lean4

theorem prod_eq_zero (h : (0 : M₀) ∈ s) : s.prod = 0 := by rcases Multiset.exists_cons_of_mem h with ⟨s', hs'⟩;
  simp [hs', Multiset.prod_cons]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru