lean_workbook_plus_15027
ProvedIf and , then prove that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15027 (a b c d : ℝ) (hab : a * b = 1) (h : a * c + b * d = 2) : c * d ≤ 1 := by sorry
Source
If and , then prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_15027 (a b c d : ℝ) (hab : a * b = 1) (h : a * c + b * d = 2) : c * d ≤ 1 := by sorry