lean_workbook_plus_61474
ProvedSolve for integers and
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_61474 (k s : ℤ) (h₁ : 7 * k - 1 = s ^ 2) : ∃ k s, 7 * k - 1 = s ^ 2 := by sorry
Source
Solve for integers and
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_61474 (k s : ℤ) (h₁ : 7 * k - 1 = s ^ 2) : ∃ k s, 7 * k - 1 = s ^ 2 := by sorry