English
If the index type is subsingleton, then from the value of the product of f over a finite set, every term on the set equals that value.
Русский
Если множество индексов является подсинглтонным, то из значения произведения следует, что каждая слагаемая равна этому значению.
LaTeX
$$$\\forall i \\in s, f(i) = b\\quad\\text{whenever } \\prod_{i\\in s} f(i) = b$$$
Lean4
/-- If a product of a `Finset` of a subsingleton type has a given
value, so do the terms in that product. -/
@[to_additive /-- If a sum of a `Finset` of a subsingleton type has a given
value, so do the terms in that sum. -/
]
theorem eq_of_subsingleton_of_prod_eq {ι : Type*} [Subsingleton ι] {s : Finset ι} {f : ι → M} {b : M}
(h : ∏ i ∈ s, f i = b) : ∀ i ∈ s, f i = b :=
Finset.eq_of_card_le_one_of_prod_eq (Finset.card_le_one_of_subsingleton s) h
