lean_workbook_plus_50

Proved

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

Hence $p={0.5\over 5.5}={1\over 11}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_50  (p : ℝ)
  (h₀ : p = 0.5 / 5.5) :
  p = 1 / 11   :=  by sorry

Source