Untitled
unknown
alda
a year ago
300 B
3
Indexable
Never
example (n : Nat): ∑ k in range (n+1), (k ^ (2 : ℕ) : ℕ) = (n*(n+1)*(2*n+1)) / 6 := by symm apply Nat.div_eq_of_eq_mul_left (by norm_num) symm induction n with | zero => simp | succ n ih => rw[sum_range_succ] rw[right_distrib] rw[ih] rw[succ_eq_add_one] ring