lean_workbook_plus_42173
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_42173 (c : ℝ) : √(c^2 - (c - 1)^2) = √(2 * c - 1) := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_42173 (c : ℝ) : √(c^2 - (c - 1)^2) = √(2 * c - 1) := by sorry