lean_workbook_plus_13306

Proved

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

The probability of not getting an event of probability p is 1-p. The probability of not getting it twice is $(1-p)(1-p)=(1-p)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13306  (p : ℝ)
  (h₀ : 0 ≤ p ∧ p ≤ 1) :
  (1 - p) * (1 - p) = (1 - p)^2   :=  by sorry

Source