Prove2Me

lean_workbook_plus_25035

Proved

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

A≡1(mod16)⇒A=16k+1.A \equiv 1 \pmod{16} \Rightarrow A = 16k+1.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_25035 (A : ℕ) (hA : A ≡ 1 [ZMOD 16]) : ∃ k : ℕ, A = 16 * k + 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph