lean_workbook_plus_22625
ProvedSolve given and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_22625 (a b x z : ℝ) : a * x = z + b ∧ b * z = x + a → (a - 1) * x + (b - 1) * z = a + b := by sorry
Source
Solve given and .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_22625 (a b x z : ℝ) : a * x = z + b ∧ b * z = x + a → (a - 1) * x + (b - 1) * z = a + b := by sorry