lean_workbook_plus_28559
ProvedGiven , prove .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_28559 (x y : ℝ) (h : x + y = 0) : (x + Real.sqrt (1 + x^2)) * (y + Real.sqrt (1 + y^2)) = 1 := by sorry
Source
Given , prove .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_28559 (x y : ℝ) (h : x + y = 0) : (x + Real.sqrt (1 + x^2)) * (y + Real.sqrt (1 + y^2)) = 1 := by sorry