Add examples and exercises form 2.1 Proving Identities in Algebraic S…

…tructures

MathLean/Ch02/ProvingAlgebraicIdentities.lean

@@ -0,0 +1,52 @@
+import MathLean.Common
+
+variable (R : Type*) [Ring R]
+
+#check (add_assoc : ∀ a b c : R, a + b + c = a + (b + c))
+#check (add_comm : ∀ a b : R, a + b = b + a)
+#check (zero_add : ∀ a : R, 0 + a = a)
+#check (neg_add_cancel : ∀ a : R, -a + a = 0)
+#check (mul_assoc : ∀ a b c : R, a * b * c = a * (b * c))
+#check (mul_one : ∀ a : R, a * 1 = a)
+#check (one_mul : ∀ a : R, 1 * a = a)
+#check (mul_add : ∀ a b c : R, a * (b + c) = a * b + a * c)
+#check (add_mul : ∀ a b c : R, (a + b) * c = a * c + b * c)
+
+variable (R : Type*) [CommRing R]
+variable (a b c d : R)
+
+example : c * b * a = b * (a * c) := by ring
+
+example : (a + b) * (a + b) = a * a + 2 * (a * b) + b * b := by ring
+
+example : (a + b) * (a - b) = a ^ 2 - b ^ 2 := by ring
+
+example (hyp : c = d * a + b) (hyp' : b = a * d) : c = 2 * a * d := by
+  rw [hyp, hyp']
+  ring
+
+namespace MyRing
+variable {R : Type*} [Ring R]
+
+theorem add_zero (a : R) : a + 0 = a := by rw [add_comm, zero_add]
+
+theorem add_right_neg (a : ℝ) : a + -a = 0 := by rw [add_comm, neg_add_cancel]
+
+#check MyRing.add_zero
+#check add_zero
+
+theorem neg_add_cancel_left (a b : R) : -a + (a + b) = b := by
+  rw [← add_assoc, neg_add_cancel, zero_add]
+
+theorem add_neg_cancel_right (a b : R) : a + b + -b = a := by
+  rw [add_comm, add_comm a b, ← add_assoc, neg_add_cancel, zero_add]
+
+theorem add_left_cancel {a b c : R} (h : a + b = a + c) : b = c := by
+  rw [← add_zero b, ← neg_add_cancel a, ← add_assoc, add_comm, ← add_assoc]
+  rw [h, add_comm, neg_add_cancel_left]
+
+theorem add_right_cancel {a b c : R} (h : a + b = c + b) : a = c := by
+  rw [← add_zero a, ← neg_add_cancel b, add_comm, add_assoc, add_comm b a]
+  rw [h, ← add_assoc, add_comm, ← add_assoc, add_comm, ← add_assoc, add_neg_cancel_right]
+
+end MyRing