lean_workbook_plus_19255

Proved

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

Again, $(9k \\pm 1)^2 \\equiv 10 (mod {27}) \\implies \\pm 18k \\equiv 9 (mod {27}) \\implies 2k \\equiv 1 (mod 3) \\implies k = 3m+2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_19255 (k : ℕ) (h₁ : (9 * k + 1) ^ 2 ≡ 10 [ZMOD 27]) : ∃ m : ℕ, k = 3 * m + 2   :=  by sorry

Source