lean_workbook_plus_78448

Proved

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

Given $x_{1}x_{2}= p^{2}+1$ and $x_{1}+x_{2}=-2m$ , show that $p^{4}+4m^{2} = (x_{1}^{2}+1)(x_{2}^{2}+1)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78448 (x₁ x₂ m p : ℤ) (h₁ : x₁ * x₂ = p^2 + 1) (h₂ : x₁ + x₂ = -2*m) : p^4 + 4*m^2 = (x₁^2 + 1)*(x₂^2 + 1)   :=  by sorry

Source