lean_workbook_plus_58808

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

$x\equiv r\mod q,y\equiv s\mod q$ ,then we have $xy\equiv rs\mod q$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58808 (x r y s : ℤ) (q : ℕ) (h₁ : x ≡ r [ZMOD q]) (h₂ : y ≡ s [ZMOD q]) :
  x * y ≡ r * s [ZMOD q]   :=  by sorry

Source