lean_workbook_plus_5920
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_5920 (c d ψ₁ ψ₂ : ℝ) : ψ₁^2 * c^2 + ψ₂^2 * d^2 ≥ -2 * c * d * ψ₁ * ψ₂ := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_5920 (c d ψ₁ ψ₂ : ℝ) : ψ₁^2 * c^2 + ψ₂^2 * d^2 ≥ -2 * c * d * ψ₁ * ψ₂ := by sorry