lean_workbook_plus_59792
ProvedSince,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59792 (a b c : ℝ) : a * b + b * c + c * a ≤ |a| * |b| + |a| * |c| + |b| * |c| := by sorry
Source
Since,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_59792 (a b c : ℝ) : a * b + b * c + c * a ≤ |a| * |b| + |a| * |c| + |b| * |c| := by sorry