prod_eq_one_iff — Mathlib

English

Equivalently, in a canonically ordered monoid, l.prod = 1 if and only if every factor is 1.

Русский

Эквивалентно: в канонически упорядоченном моноиде l.prod = 1 тогда и только тогда, когда каждый элемент равен 1.

LaTeX

$$$\\forall l:\\, \\text{List } M,\\ l.prod = 1 \\iff \\forall x\\in l,\\ x = 1.$$

Lean4

@[to_additive]
theorem prod_eq_one_iff [IsOrderedMonoid M] : l.prod = 1 ↔ ∀ x ∈ l, x = (1 : M) :=
  ⟨all_one_of_le_one_le_of_prod_eq_one fun _ _ => one_le _, fun h =>
    by
    rw [List.eq_replicate_iff.2 ⟨_, h⟩, prod_replicate, one_pow]
    · exact (length l)
    · rfl⟩

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