lean_workbook_plus_77838
Proved4n \equiv 4 (\mod 12) \Rightarrow n-1 \equiv 0 (\mod 3) \Rightarrow n \equiv 1 (\mod 3)$ .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_77838 (n : ℕ) : (4*n ≡ 4 [ZMOD 12] → n-1 ≡ 0 [ZMOD 3] → n ≡ 1 [ZMOD 3]) := by sorry
Source