lean_workbook_plus_6771
ProvedGiven , where and are integers with being prime, show that and discuss the possible values of when .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_6771 (n m : ℤ) (p : ℕ) (hp : p.Prime) (h : n = m * p) : (n + p^2) / p = m + p := by sorry
Source