lean_workbook_plus_42865

Proved

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

Derive the identity $\frac{x^{a}}{(1-x)^{a+1}}\frac{x^{b}}{(1-x)^{b+1}}= \frac{x^{a+b}}{(1-x)^{a+b+2}}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42865 (a b : ℕ) (x : ℝ) (hx : 0 < x ∧ x < 1) :
  x^a / (1 - x)^(a + 1) * (x^b / (1 - x)^(b + 1)) = x^(a + b) / (1 - x)^(a + b + 2)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph