Prove2Me

lean_workbook_plus_35679

Proved

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

If a≡b (mod m)a\equiv b \ (mod \ m) and p≡q (mod m)p\equiv q \ (mod \ m), prove that ab≡pq (mod m)ab\equiv pq \ (mod \ m) and a+b≡p+q (mod m)a+b\equiv p+q \ (mod \ m) .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_35679 (a b m : ℕ) (p q : ℕ) (h1 : a ≡ b [ZMOD m]) (h2 : p ≡ q [ZMOD m]) : a * p ≡ b * q [ZMOD m] ∧ a + p ≡ b + q [ZMOD m]   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph