lean_workbook_plus_46589

Proved

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

$A$ is $\equiv -1 \mod 8$ and $\equiv -1 \mod 3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46589 (A : ℕ) (hA : A ≡ -1 [ZMOD 8]) (hA' : A ≡ -1 [ZMOD 3]) : ∃ B : ℕ, B ≡ A [ZMOD 8] ∧ B ≡ A [ZMOD 3]   :=  by sorry

Source