Prove2Me

lean_workbook_plus_34642

Proved

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

Prooving the converse: \n (a+b)2=a2+2ab+b2⇒(a+b)(a+b)=a2+2ab+b2⇒a2+ab+ba+b2=a2+2ab+b2⇒ab+ba=2ab=ab+ab⇒ab=ba\begin{array}{l}(a + b)^2 = {a^2} + 2ab + {b^2} \Rightarrow (a + b)(a + b) = {a^2} + 2ab + {b^2} \\\Rightarrow {a^2} + ab + ba + {b^2} = {a^2} + 2ab + {b^2} \Rightarrow ab + ba = 2ab = ab + ab \Rightarrow ab = ba\end{array}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_34642  (a b : ℝ)
  (h₀ : (a + b)^2 = a^2 + 2 * a * b + b^2) :
  a * b = b * a   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph