lean_workbook_plus_38597
Disprovedwhich says .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38597 : ∀ a b c : ℝ, 1 = a^2 * b^3 * c^4 → a * b ≥ 1 := by sorry
Source
which says .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_38597 : ∀ a b c : ℝ, 1 = a^2 * b^3 * c^4 → a * b ≥ 1 := by sorry