English
Let c be a congruence on a CommMonoid M and s a finite set (Finset) of indices with f,g : ι → M. If c(f(i)) (g(i)) for all i ∈ s, then c (∏_{i∈s} f(i)) (∏_{i∈s} g(i)).
Русский
Пусть c — конгруэнция на CommMonoid M и s — конечный набор индексов. Если для каждого i ∈ s выполняется c(f(i)) (g(i)), то произведение по i∈s f(i) и произведение по i∈s g(i) эквивалентны по c.
LaTeX
$$$c\\left(\\prod_{i\\in s} f(i)\\right)\\left(\\prod_{i\\in s} g(i)\\right)$$$
Lean4
/-- Multiplicative congruence relations preserve finite product. -/
@[to_additive /-- Additive congruence relations preserve finite sum. -/
]
protected theorem finset_prod {ι M : Type*} [CommMonoid M] (c : Con M) (s : Finset ι) {f g : ι → M}
(h : ∀ i ∈ s, c (f i) (g i)) : c (s.prod f) (s.prod g) :=
c.multiset_prod h
