lean_workbook_plus_31673
ProvedProve that for
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_31673 (a : ℝ) (ha : 1 < a) : a^2 / (a - 1) ≥ 4 := by sorry
Source
Prove that for
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_31673 (a : ℝ) (ha : 1 < a) : a^2 / (a - 1) ≥ 4 := by sorry