multiset_prod_pos — Mathlib

English

For a multiset of elements in a canonically ordered add, the product is positive iff every element is positive.

Русский

Для мульти множества элементов в канонически упорядоченном дополнении произведение положительно тогда и только тогда, когда каждый элемент положителен.

LaTeX

$$$0 < m.prod \; \Longleftrightarrow \forall x \in m, 0 < x$$$

Lean4

@[simp]
theorem multiset_prod_pos {R : Type*} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [NoZeroDivisors R]
    [Nontrivial R] {m : Multiset R} : 0 < m.prod ↔ ∀ x ∈ m, 0 < x :=
  by
  rcases m with ⟨l⟩
  rw [Multiset.quot_mk_to_coe'', Multiset.prod_coe]
  exact CanonicallyOrderedAdd.list_prod_pos

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