mul — Mathlib

English

If x1 ≡ y1 mod I and x2 ≡ y2 mod I in a commutative ring A with ideal I, then x1 x2 ≡ y1 y2 mod I.

Русский

Если x1 ≡ y1 mod I и x2 ≡ y2 mod I в кольце A с идеалом I, то x1 x2 ≡ y1 y2 mod I.

LaTeX

$$$$ x_1 \\equiv y_1\\ [SMOD\\ I] \\land x_2 \\equiv y_2\\ [SMOD\\ I] \\Rightarrow x_1 x_2 \\equiv y_1 y_2\\ [SMOD\\ I]. $$$$

Lean4

@[gcongr]
theorem mul {I : Ideal A} {x₁ x₂ y₁ y₂ : A} (hxy₁ : x₁ ≡ y₁ [SMOD I]) (hxy₂ : x₂ ≡ y₂ [SMOD I]) :
    x₁ * x₂ ≡ y₁ * y₂ [SMOD I] :=
  by
  simp only [SModEq.def, Ideal.Quotient.mk_eq_mk, map_mul] at hxy₁ hxy₂ ⊢
  rw [hxy₁, hxy₂]

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