lean_workbook_plus_43735

Proved

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

Given $P_n = \frac {3n^2 - n}{2}, T_{n-1} = \frac {(n-1)(n)}{2}$ , prove that $P_n=3T_{n-1}+n$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_43735 (n : ℕ) : 3 * ((n - 1) * n) / 2 + n = (3 * n ^ 2 - n) / 2   :=  by sorry

Source