lean_workbook_plus_48930
ProvedFactor the expression .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48930 (x : ℤ) : x^4 + 1 = (x^2 - √2*x + 1) * (x^2 + √2*x + 1) := by sorry
Source
Factor the expression .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_48930 (x : ℤ) : x^4 + 1 = (x^2 - √2*x + 1) * (x^2 + √2*x + 1) := by sorry