length_pos_of_one_lt_prod — Mathlib

English

If a list L in a monoid M has product greater than 1 (with a preorder), then L is nonempty.

Русский

Если произведение элементов списка L в моноиде M превосходит единицу (в предустановленном порядке), то список непуст.

LaTeX

$$$ 0 < L.length \text{ given } 1 < L.prod $$$

Lean4

/-- A list with product greater than one must have positive length. -/
@[to_additive length_pos_of_sum_pos /-- A list with positive sum must have positive length. -/
    ]
theorem length_pos_of_one_lt_prod [Preorder M] (L : List M) (h : 1 < L.prod) : 0 < L.length :=
  length_pos_of_prod_ne_one L h.ne'

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