Exercises Added.

Exercises/Exercise1.lean

@@ -0,0 +1,14 @@
+import Mathlib
+
+open Finset BigOperators
+
+/-
+  If a and r are real numbers and r ≠ 1, then
+  ∑_{j=0}^{n}
+  a * r^i = (a * r^(n+1) - a) / (r-1).
+-/
+
+example {a r : ℝ} (n : ℕ) (h : r ≠ 1) :
+  ∑ i ∈ range (n+1),
+  a * r^i = (a * r^(n+1) - a) / (r-1) := by
+  sorry

Exercises/Exercise2.lean

@@ -0,0 +1,9 @@
+import Mathlib
+
+open Nat
+
+/-
+  Let n and k be non-negative integers with k ≤ n. Then
+  (i) binom n 0 = binom n n = 1
+  (ii) binom n k = binom n (n - k)
+-/

Exercises/Exercise3.lean

@@ -0,0 +1,12 @@
+import Mathlib
+
+open Nat
+
+/-
+  We define a function recursively for all positive integers n by
+  f(1) = 1, f(2) = 5, and
+  for n > 2, f(n + 1) = f(n) + 2 * f(n - 1).
+
+  Show that f(n) = 2^n + (-1)^n,
+  using the second principle of mathematical induction.
+-/