lean_workbook_plus_51566

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

b) Sub in $s=0$ \n $0=-4.9t^{2}+20t$ \n $-4.9t\left(t-\frac{200}{49}\right)=0$ \n $t=0,\frac{200}{49}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_51566  (t : ℝ)
  (h₀ : -4.9 * t^2 + 20 * t = 0) :
  t = 0 ∨ t = 200 / 49   :=  by sorry

Source