add — Mathlib

English

Let U be a submodule of M. If x1 ≡ y1 mod U and x2 ≡ y2 mod U, then x1 + x2 ≡ y1 + y2 mod U.

Русский

Пусть U — подпомодуль M. Если x1 ≡ y1 по модулю U и x2 ≡ y2 по модулю U, то x1 + x2 ≡ y1 + y2 по модулю U.

LaTeX

$$$$ (x_1 \\equiv y_1\\ [SMOD\\ U]) \\land (x_2 \\equiv y_2\\ [SMOD\\ U]) \\Rightarrow (x_1 + x_2) \\equiv (y_1 + y_2)\\ [SMOD\\ U]. $$$$

Lean4

@[gcongr]
theorem add (hxy₁ : x₁ ≡ y₁ [SMOD U]) (hxy₂ : x₂ ≡ y₂ [SMOD U]) : x₁ + x₂ ≡ y₁ + y₂ [SMOD U] :=
  by
  rw [SModEq.def] at hxy₁ hxy₂ ⊢
  simp_rw [Quotient.mk_add, hxy₁, hxy₂]

Похожие утверждения