prod_eq_one_iff — Mathlib

English

For an ordered monoid, the product of m elements equals 1 if and only if every element equals 1.

Русский

Для упорядоченного монада произведение равно 1 тогда и только тогда, когда каждый элемент равен 1.

LaTeX

$$$ m.prod = 1 \;\iff\; \forall x ∈ m, x = 1 $$$

Lean4

@[to_additive]
theorem prod_eq_one_iff [IsOrderedMonoid α] : m.prod = 1 ↔ ∀ x ∈ m, x = (1 : α) :=
  Quotient.inductionOn m fun l ↦ by simpa using List.prod_eq_one_iff

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