lean_workbook_plus_71983
ProvedRewrite as , so
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71983 (p q : ℝ) : 4 * q < 4 * p - 1 ↔ q < p - 1 / 4 := by sorry
Source
Rewrite as , so
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_71983 (p q : ℝ) : 4 * q < 4 * p - 1 ↔ q < p - 1 / 4 := by sorry