lean_workbook_plus_44352
ProvedIf then prove .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_44352 (x y : ℝ) (h : (x + Real.sqrt (x^2 + 1)) * (y + Real.sqrt (y^2 + 1)) = 0) : x + y = 0 := by sorry
Source
If then prove .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_44352 (x y : ℝ) (h : (x + Real.sqrt (x^2 + 1)) * (y + Real.sqrt (y^2 + 1)) = 0) : x + y = 0 := by sorry