prod_eq_one — Mathlib

English

If every element of a list is equal to 1 (in a monoid), then the product of the whole list is 1.

Русский

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

LaTeX

$$$ (\forall x \in l, x = 1) \Rightarrow l.prod = 1 $$$

Lean4

@[to_additive]
theorem prod_eq_one (hl : ∀ x ∈ l, x = 1) : l.prod = 1 := by
  induction l with
  | nil => rfl
  | cons i l hil => rw [List.prod_cons, hil fun x hx ↦ hl _ (mem_cons_of_mem i hx), hl _ mem_cons_self, one_mul]

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