exists_mem_ne_one_of_prod_ne_one — Mathlib

English

If a list L has product different from 1, then there exists an element x in L such that x ≠ 1.

Русский

Если произведение элементов списка L не равно 1, то существует элемент x в L такой, что x ≠ 1.

LaTeX

$$$ l.prod \neq 1 \rightarrow \exists x \in l, x \neq 1 $$$

Lean4

@[to_additive]
theorem exists_mem_ne_one_of_prod_ne_one (h : l.prod ≠ 1) : ∃ x ∈ l, x ≠ (1 : M) := by
  simpa only [not_forall, exists_prop] using mt prod_eq_one h

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