sub — Mathlib

English

If x1 ≡ y1 mod U and x2 ≡ y2 mod U, then x1 − x2 ≡ y1 − y2 mod U.

Русский

Если x1 ≡ y1 mod U и x2 ≡ y2 mod U, то x1 − x2 ≡ y1 − y2 mod 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 sub (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_sub, hxy₁, hxy₂]

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