lean_workbook_plus_27685
ProvedWe have :
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27685 (a : ℝ) : a^2 + 1 ≥ a := by sorry
Source
We have :
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_27685 (a : ℝ) : a^2 + 1 ≥ a := by sorry