lean_workbook_plus_73133

Proved

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

x^2+y^2+6xy=z^2 $\iff$ x(x+6y)=(z-y)(z+y)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_73133 : ∀ x y z : ℤ, x^2 + y^2 + 6 * x * y = z^2 ↔ x * (x + 6 * y) = (z - y) * (z + y)   :=  by sorry

Source