all_one_of_le_one_le_of_prod_eq_one

English

If a multiset s has all elements at least 1 and its product equals 1, then every element in s is equal to 1.

Русский

Если произведение элементов мульти-множества равно 1 и каждый элемент не меньше 1, то все элементы равны 1.

LaTeX

$$$ \left( \forall x \in s, 1 \le x \right) \wedge s.prod = 1 \Rightarrow \forall x \in s, 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 [IsOrderedMonoid α] :
    (∀ x ∈ s, (1 : α) ≤ x) → s.prod = 1 → ∀ x ∈ s, x = (1 : α) :=
  Quotient.inductionOn s
    (by
      simp only [quot_mk_to_coe, prod_coe, mem_coe]
      exact fun l => List.all_one_of_le_one_le_of_prod_eq_one)

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