lean_workbook_plus_57477
ProvedProve that , where .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_57477 (t : ℝ) (ht : 0 ≤ t ∧ t ≤ 1) : 6303 * t ^ 5 + 3320 * t ^ 4 + 1776 ≥ 5656 * t ^ 3 := by sorry
Source
Prove that , where .
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_57477 (t : ℝ) (ht : 0 ≤ t ∧ t ≤ 1) : 6303 * t ^ 5 + 3320 * t ^ 4 + 1776 ≥ 5656 * t ^ 3 := by sorry