Prove2Me

lean_workbook_plus_75810

Proved

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

Therefore, the answer is all positive integers nn , such that n≡4(mod6)\boxed{n\equiv4\pmod6} .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_75810 : {n : ℕ | n ≡ 4 [ZMOD 6]} = {n : ℕ | 0 < n ∧ n ≡ 4 [ZMOD 6]}   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph