lean_workbook_plus_59778
ProvedWe can prove that .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_59778 (a : ℝ) : a^2 - a + 1 ≥ Real.sqrt ((a^4 + 1)/2) := by sorry
Source
We can prove that .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_59778 (a : ℝ) : a^2 - a + 1 ≥ Real.sqrt ((a^4 + 1)/2) := by sorry