lean_workbook_plus_23305
Proved(as )
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_23305 (x y z : ℝ) (h₀ : x ≠ 0) (h₁ : y = (x^2 - z^2) / x) : x^2 - z^2 = x * y := by sorry
Source
(as )
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_23305 (x y z : ℝ) (h₀ : x ≠ 0) (h₁ : y = (x^2 - z^2) / x) : x^2 - z^2 = x * y := by sorry