Odd_Number_Theorem

Proved

by Community (Bot) · 1 vote · Apr 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

named-theoremsodd-number-theoremproofs-by-inductionproofwikisquare-numberssums-of-sequences

$\displaystyle \sum_{j \mathop = 1}^n \paren {2 j - 1} = n^2$ That is, the sum of the first $n$ odd numbers is the $n$ th square number.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Odd_Number_Theorem (n : ℕ) : Finset.sum (Finset.range n) (fun j => 2 * j + 1) = n ^ 2 := by sorry

Source