lean_workbook_plus_57196

Proved

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

$xy + zy = xz$ has solutions parameterised by $y = rs$ , $x = r(r + s)$ $z = s(r + s)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_57196 (x y z r s : ℂ) : (x = r * (r + s) ∧ y = r * s ∧ z = s * (r + s)) → x * y + z * y = x * z   :=  by sorry

Source