lean_workbook_plus_10726
ProvedProve that for all real numbers and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10726 (p q : ℝ) : (p^2 + 1) * (q^2 + 1) ≥ (1 + p * q)^2 := by sorry
Source
Prove that for all real numbers and .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_10726 (p q : ℝ) : (p^2 + 1) * (q^2 + 1) ≥ (1 + p * q)^2 := by sorry