lean_workbook_plus_9174

Proved

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

The probability that two adjacent digits are different is $2\cdot \frac{15}{24} \cdot \frac{9}{23} = \frac{45}{92}.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9174 :
  ((2 : ℝ) * 15 / 24 * (9 / 23)) = 45 / 92   :=  by sorry

Source