multiset_prod_eq_bot — Mathlib

English

In an integral domain, a finite multiset product of ideals is zero if and only if one of the terms is the zero ideal.

Русский

В интегральной области произведение конечного мультизеяда идеалов равно нулю тогда и только тогда, когда хотя бы один член равен нулевому идеалу.

LaTeX

$$$$ s.\prod = \bot \iff \bot \in s $$$$

Lean4

/-- A product of ideals in an integral domain is zero if and only if one of the terms is zero. -/
@[simp]
theorem multiset_prod_eq_bot {R : Type*} [CommSemiring R] [IsDomain R] {s : Multiset (Ideal R)} : s.prod = ⊥ ↔ ⊥ ∈ s :=
  Multiset.prod_eq_zero_iff

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