all_one_of_le_one_le_of_prod_eq_one

English

For a commutative ordered monoid with canonically ordered multiplication, the product of a list equals 1 if and only if every factor equals 1.

Русский

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

LaTeX

$$$\\forall l:\\, \\text{List } M,\\ l.prod = 1 \\iff \\forall x\\in l,\\ x = 1.$$

Lean4

@[to_additive all_zero_of_le_zero_le_of_sum_eq_zero]
theorem all_one_of_le_one_le_of_prod_eq_one [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : List M}
    (hl₁ : ∀ x ∈ l, (1 : M) ≤ x) (hl₂ : l.prod = 1) {x : M} (hx : x ∈ l) : x = 1 :=
  _root_.le_antisymm (hl₂ ▸ single_le_prod hl₁ _ hx) (hl₁ x hx)

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