English
If x_i ≡ y_i mod I for all i in a finite index set, then ∏ x_i ≡ ∏ y_i mod I.
Русский
Если для всех i в конечном множестве индексов x_i ≡ y_i mod I, тогда произведения по i удовлетворяют ∏ x_i ≡ ∏ y_i mod I.
LaTeX
$$$$ \\left( \\forall i \\in s,\\ x_i \\equiv y_i\\ [SMOD\\ I] \\right) \\Rightarrow \\left( \\prod_{i \\in s} x_i \\equiv \\prod_{i \in s} y_i\\ [SMOD\\ I] \\right). $$$$
Lean4
@[gcongr]
theorem prod {I : Ideal A} {ι} {s : Finset ι} {x y : ι → A} (hxy : ∀ i ∈ s, x i ≡ y i [SMOD I]) :
∏ i ∈ s, x i ≡ ∏ i ∈ s, y i [SMOD I] := by
classical
induction s using Finset.cons_induction with
| empty => simp [SModEq.rfl]
| cons i s _ ih =>
grw [Finset.prod_cons, Finset.prod_cons, hxy i (Finset.mem_cons_self i s),
ih (fun j hj ↦ hxy j (Finset.mem_cons_of_mem hj))]
