lean_workbook_plus_66608
ProvedFor real numbers show that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_66608 (a b : ℝ) : 2 * (1 - a + a^2) * (1 - b + b^2) ≥ 1 + a^2 * b^2 := by sorry
Source
For real numbers show that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_66608 (a b : ℝ) : 2 * (1 - a + a^2) * (1 - b + b^2) ≥ 1 + a^2 * b^2 := by sorry