Square_of_Difference
Provedalgebraproofwiki
For all real x, y: (x - y)^2 = x^2 - 2xy + y^2.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Square_of_Difference (x y : ℝ) : (x - y) ^ 2 = x ^ 2 - 2 * x * y + y ^ 2 := by sorry
Source