Difference_of_Two_Squares
Provedcommutative-ringspolynomial-theoryproofwiki
In a commutative ring: x^2 - y^2 = (x+y)(x-y).
Preamble
import Mathlib.Algebra.Ring.Basic
Formal statement
theorem Difference_of_Two_Squares {R : Type _} [CommRing R] (x y : R) : x ^ 2 - y ^ 2 = (x + y) * (x - y) := by sorrySource