lean_workbook_plus_58532
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_58532 : ∀ a b c : ℝ, c * (c + a) + b * (a + b) = (a + b) * (c + a) ↔ a^2 = b^2 + c^2 - b * c := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_58532 : ∀ a b c : ℝ, c * (c + a) + b * (a + b) = (a + b) * (c + a) ↔ a^2 = b^2 + c^2 - b * c := by sorry