lean_workbook_plus_16214

Proved

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

Note that the given condition implies that $ab^2=b$ . It is easy to see that for all positive integers $k$ , we have $a^kb^{k+1}=b$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_16214 (a b : ℕ) (h : a * b ^ 2 = b) : ∀ k : ℕ, a ^ k * b ^ (k + 1) = b   :=  by sorry

Source