lean_workbook_plus_27772
ProvedThe domain of the definition is:
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27772 (t : ℝ) : (t < -3/2 ∨ 3/2 < t) → 0 < (t^2 - 9/4) := by sorry
Source
The domain of the definition is:
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_27772 (t : ℝ) : (t < -3/2 ∨ 3/2 < t) → 0 < (t^2 - 9/4) := by sorry