lean_workbook_plus_60649
ProvedProve the inequality for complex numbers and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_60649 (x y : ℂ) : ‖x * y‖ ≤ (1 / 2) * (‖x‖ ^ 2 + ‖y‖ ^ 2) := by sorry
Source
Prove the inequality for complex numbers and .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_60649 (x y : ℂ) : ‖x * y‖ ≤ (1 / 2) * (‖x‖ ^ 2 + ‖y‖ ^ 2) := by sorry