lean_workbook_plus_13131
ProvedProve that where
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_13131 (m : ℝ) (h : m ≥ 0) : 2 * m ^ 3 + 12 * m ^ 2 + 15 * m ≥ 0 := by sorry
Source
Prove that where
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_13131 (m : ℝ) (h : m ≥ 0) : 2 * m ^ 3 + 12 * m ^ 2 + 15 * m ≥ 0 := by sorry