lean_workbook_plus_81052

Proved

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

Solve for $x$ and $y$ in the system of congruences: $9x + 12y \equiv 4 \mod 47$ and $6x + 7y \equiv 14 \mod 47$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81052 (x y : ℕ) (h1 : 9*x + 12*y ≡ 4 [ZMOD 47]) (h2 : 6*x + 7*y ≡ 14 [ZMOD 47]) : x ≡ 26 [ZMOD 47] ∧ y ≡ 20 [ZMOD 47]   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph