length_pos_of_prod_ne_one — Mathlib

English

For a list L in a monoid M, if its product is not equal to the unit 1, then L is nonempty (length > 0).

Русский

Для списка L из моноида M, если произведение элементов списка не равно единице, то список непуст: длина больше нуля.

LaTeX

$$$ L.prod \neq 1 \Rightarrow 0 < L.length $$$

Lean4

/-- A list with product not one must have positive length. -/
@[to_additive /-- A list with sum not zero must have positive length. -/
    ]
theorem length_pos_of_prod_ne_one (L : List M) (h : L.prod ≠ 1) : 0 < L.length :=
  by
  cases L
  · simp at h
  · simp

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