Add exercises to Calculating.lean

GrahamStrickland · Jan 7, 2025 · 6443436 · 6443436
1 parent aa24fd3
commit 6443436
Showing 1 changed file with 11 additions and 0 deletions.
diff --git a/MathLean/Ch02/Calculating.lean b/MathLean/Ch02/Calculating.lean
@@ -0,0 +1,11 @@
+import MathLean.Common
+
+example (a b c : ℝ) : a * b * c = b * (a * c) := by
+  rw [mul_comm a b]
+  rw [mul_assoc b a c]
+
+example (a b c : ℝ) : c * b * a = b * (a * c) := by
+  sorry
+
+example (a b c : ℝ) : a * (b * c) = b * (a * c) := by
+  sorry