Prove2Me

lean_workbook_plus_38370

Proved

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

Explain the steps in the solution: (n2)−n=n(n−1)2−n=n(n−3)2 \binom{n}{2}-n = \frac{n(n-1)}{2}-n = \frac{n(n-3)}{2}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38370 (n : ℕ) : (n.choose 2) - n = n * (n - 3) / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph