English
A RingCon relation t preserves the sum of matched pairs over a finite list: if t(f(i)) relates to g(i) for all i in the list, then t(sum f(i)) relates to sum g(i).
Русский
Отношение RingCon сохраняет сумму в списке: если для всех элементов i списка выполняется t(f(i)) ∼ g(i), то t(сумма f(i)) ∼ сумма g(i).
LaTeX
$$$$ \forall l\: \text{List}, \; (\forall i \in l,\ t(f(i), g(i))) \Rightarrow t(\sum_{i\in l} f(i), \sum_{i\in l} g(i)) $$$$
Lean4
/-- Congruence relation of a ring preserves finite sum indexed by a list. -/
protected theorem listSum {ι S : Type*} [AddMonoid S] [Mul S] (t : RingCon S) (l : List ι) {f g : ι → S}
(h : ∀ i ∈ l, t (f i) (g i)) : t (l.map f).sum (l.map g).sum :=
t.toAddCon.list_sum h
