English
In a monoid where the only unit is 1, the product over a set equals 1 if and only if every factor equals 1.
Русский
В моноиде, где единственный единичный элемент — 1, произведение по множеству равно 1 тогда и только тогда, когда каждый фактор равен 1.
LaTeX
$$$\\text{If } \\text{the only unit of } M \\text{ is } 1, \\; \\prod_{i \\in s} f(i) = 1 \\;\\Leftrightarrow\\; \\forall i \\in s, f(i)=1$$$
Lean4
/-- In a monoid whose only unit is `1`, a product is equal to `1` iff all factors are `1`. -/
@[to_additive (attr := simp) /--
In an additive monoid whose only unit is `0`, a sum is equal to `0` iff all terms are `0`. -/
]
theorem prod_eq_one_iff [Subsingleton Mˣ] : ∏ i ∈ s, f i = 1 ↔ ∀ i ∈ s, f i = 1 := by
induction s using Finset.cons_induction <;> simp [*]
