lean_workbook_plus_1826
ProvedProve the inequality .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1826 (x y : ℝ) : (|x| + |y|) ^ 2 ≥ (|x + y|) ^ 2 := by sorry
Source
Prove the inequality .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_1826 (x y : ℝ) : (|x| + |y|) ^ 2 ≥ (|x + y|) ^ 2 := by sorry