English
Let c be a congruence on a MulOneClass M and l a finite list of indices with functions f,g : ι → M. If c(f(x)) (g(x)) for all x in l, then c of the product over the list of f equals the product over the list of g.
Русский
Пусть c—конгруэнция на MulOneClass M, и l — конечный список индексов с функциями f,g: ι → M. Если c(f(x)) (g(x)) для каждого x в l, то произведение по списку f и произведение по списку g эквивалентны по c.
LaTeX
$$$\\forall l:\\\ \text{List ι},\\forall f,g:\\ ι\\to M,\\ (\\forall x\\in l,\; c(f(x),g(x)))\\Rightarrow c\\left(\\prod_{x\\in l} f(x)\\right)\\left(\\prod_{x\\in l} g(x)\\right)$$$
Lean4
/-- Multiplicative congruence relations preserve product indexed by a list. -/
@[to_additive /-- Additive congruence relations preserve sum indexed by a list. -/
]
protected theorem list_prod {ι M : Type*} [MulOneClass M] (c : Con M) {l : List ι} {f g : ι → M}
(h : ∀ x ∈ l, c (f x) (g x)) : c (l.map f).prod (l.map g).prod := by
induction l with
| nil => simpa only [List.map_nil, List.prod_nil] using c.refl 1
| cons x xs ih =>
rw [List.map_cons, List.map_cons, List.prod_cons, List.prod_cons]
exact c.mul (h _ <| .head _) <| ih fun k hk ↦ h _ (.tail _ hk)
