Sophie_Germains_Identity
Provedalgebrapolynomial-identitiesproofwiki
For all integers x, y: x^4 + 4y^4 = (x^2 + 2y^2 + 2xy)(x^2 + 2y^2 - 2x*y).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Sophie_Germains_Identity (x y : ℤ) : x ^ 4 + 4 * y ^ 4 = (x ^ 2 + 2 * y ^ 2 + 2 * x * y) * (x ^ 2 + 2 * y ^ 2 - 2 * x * y) := by sorry
Source