lean_workbook_plus_76811
ProvedThus, the solution set is for .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_76811 (k : ℤ) : (∃ n : ℤ, k = 13*n + 4) ↔ (k ≡ 4 [ZMOD 13]) := by sorry
Source
Thus, the solution set is for .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_76811 (k : ℤ) : (∃ n : ℤ, k = 13*n + 4) ↔ (k ≡ 4 [ZMOD 13]) := by sorry