lean_workbook_plus_48801
OpenLetting be the original number of bacteria and be the number of hours it takes for the initial number of bacteria to decrease by , we have , so . Taking the logarithm, we have . By the Change of Base Formula, this is . Plugging this into a calculator we get hours.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48801 (n : ℝ) (h : ℝ) (h₀ : 0 < n) (h₁ : 0 < h) (h₂ : (0.9^h) * n = 0.5 * n) : h = Real.log 0.5 / Real.log 0.9 := by sorry
Source