English
Let s be a finite index set and x_i, y_i a family of M-valued elements. If for every i in s, x_i ≡ y_i mod U, then the sums over i ∈ s satisfy ∑ x_i ≡ ∑ y_i mod U.
Русский
Пусть s — конечный множество индексов, и пусть {x_i}, {y_i} — семейства элементов M. Если для каждого i ∈ s выполняется x_i ≡ y_i mod U, то ∑_{i∈s} x_i ≡ ∑_{i∈s} y_i mod U.
LaTeX
$$$$ \\left( \\forall i \\in s,\\ x_i \\equiv y_i\\ [SMOD\\ U] \\right) \\Rightarrow \\left( \\sum_{i \\in s} x_i \\equiv \\sum_{i \\in s} y_i\\ [SMOD\\ U] \\right). $$$$
Lean4
@[gcongr]
theorem sum {ι} {s : Finset ι} {x y : ι → M} (hxy : ∀ i ∈ s, x i ≡ y i [SMOD U]) :
∑ i ∈ s, x i ≡ ∑ i ∈ s, y i [SMOD U] := by
classical
induction s using Finset.cons_induction with
| empty => simp [SModEq.rfl]
| cons i s _ ih =>
grw [Finset.sum_cons, Finset.sum_cons, hxy i (Finset.mem_cons_self i s),
ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]
