lean_workbook_plus_14134
DisprovedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_14134 : ∀ x : ℝ, x * Real.sqrt ((x - 1) / (x + 1)) = (x / (x + 1)) * Real.sqrt (x ^ 2 - 1) := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_14134 : ∀ x : ℝ, x * Real.sqrt ((x - 1) / (x + 1)) = (x / (x + 1)) * Real.sqrt (x ^ 2 - 1) := by sorry