lean_workbook_plus_17172
ProvedProve that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_17172 (x y : ℝ) : (1 + x ^ 2) * (1 + y ^ 2) ≥ (1 + x * y) ^ 2 := by sorry
Source
Prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_17172 (x y : ℝ) : (1 + x ^ 2) * (1 + y ^ 2) ≥ (1 + x * y) ^ 2 := by sorry