lean_workbook_plus_20973

Proved

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

Induction on $n$ . For prime $p$ such that $\gcd (p,a)= \gcd (p,b)=1$ then for each $n$ , there exists $x_n,y_n$ such that $p^n \mid ax_n^2+by_n^2-1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_20973 (p a b : ℕ) (hp : p.Prime) (hab : a ≠ 0 ∧ b ≠ 0) (hgcd1 : Nat.Coprime a p) (hgcd2 : Nat.Coprime b p) : ∀ n : ℕ, ∃ x y : ℕ, p ^ n ∣ a * x ^ 2 + b * y ^ 2 - 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph