lean_workbook_plus_73732
ProvedShow that ( If and only if )
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_73732 (x y : ℝ) : |x + y| = |x| + |y| ↔ x*y ≥ 0 := by sorry
Source
Show that ( If and only if )
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_73732 (x y : ℝ) : |x + y| = |x| + |y| ↔ x*y ≥ 0 := by sorry