English
Let c be a congruence on a CommMonoid M and s a multiset of indices with f,g : ι → M. If every x ∈ s satisfies c(f x) (g x), then c of the product over s of f equals the product over s of g.
Русский
Пусть c — конгруэнция на CommMonoid M, и s — мульти-множество индексов с f,g : ι → M. Если для каждого x ∈ s выполняется c(f x) (g x), то произведение по s от f эквивалентно произведению по s от g по отношению c.
LaTeX
$$$c\\left(\\prod_{x\\in s} f(x)\\right)\\left(\\prod_{x\\in s} g(x)\\right)$$$
Lean4
/-- Multiplicative congruence relations preserve product indexed by a multiset. -/
@[to_additive /-- Additive congruence relations preserve sum indexed by a multiset. -/
]
protected theorem multiset_prod {ι M : Type*} [CommMonoid M] (c : Con M) {s : Multiset ι} {f g : ι → M}
(h : ∀ x ∈ s, c (f x) (g x)) : c (s.map f).prod (s.map g).prod := by rcases s; simpa using c.list_prod h
