lean_workbook_plus_76434
ProvedProve that :
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_76434 (u v : ℂ) : ‖u + v‖^2 + ‖u - v‖^2 = 2 * (‖u‖^2 + ‖v‖^2) := by sorry
Source
Prove that :
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_76434 (u v : ℂ) : ‖u + v‖^2 + ‖u - v‖^2 = 2 * (‖u‖^2 + ‖v‖^2) := by sorry