lean_workbook_plus_4979

Proved

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

Let $r$ be Rudolph's rate (mph). Since $50=r\cdot t$ , the time that it takes him to bike 50 miles is $\frac{50}{r}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4979 (r t : ℝ) (h₁ : r * t = 50) : t = 50 / r   :=  by sorry

Source