English
Let t be a ring congruence on a ring S. For any finite index set ι and functions f,g: ι → S, if t(f(i), g(i)) for every i in a finite subset s, then t(sum_{i∈s} f(i)) (sum_{i∈s} g(i)).
Русский
Пусть t — конгруэнция кольца S. Для любого множества индексов ι и функций f,g: ι → S, если t(f(i), g(i)) для каждого i ∈ s для конечного множества s, тогда t(∑_{i∈s} f(i)) (∑_{i∈s} g(i)).
LaTeX
$$$$\forall ι\ S\ [AddCommMonoid S]\ [Mul S]\ (t : RingCon S)\ (s : Finset ι)\ (f g : ι \to S),\ (\forall i \in s, t (f i) (g i)) \Rightarrow t (s.sum f) (s.sum g).$$$$
Lean4
/-- Congruence relation of a ring preserves finite sum. -/
protected theorem finsetSum {ι S : Type*} [AddCommMonoid S] [Mul S] (t : RingCon S) (s : Finset ι) {f g : ι → S}
(h : ∀ i ∈ s, t (f i) (g i)) : t (s.sum f) (s.sum g) :=
t.toAddCon.finset_sum s h
