From 7d6ba8fcdb51488a41f5ec1ab4e832eefce9e46a Mon Sep 17 00:00:00 2001
From: SinTan1729 <sayantan.santra689@gmail.com>
Date: Wed, 7 Feb 2024 16:47:21 -0600
Subject: [PATCH] new: Added references

---
 LeanTalkSP24/basics2.lean | 5 +++--
 references.md             | 6 ++++++
 2 files changed, 9 insertions(+), 2 deletions(-)
 create mode 100644 references.md

diff --git a/LeanTalkSP24/basics2.lean b/LeanTalkSP24/basics2.lean
index d447f8b..8aa7671 100644
--- a/LeanTalkSP24/basics2.lean
+++ b/LeanTalkSP24/basics2.lean
@@ -23,9 +23,10 @@ def IsOdd (n : ℕ) : Bool := ¬IsEven n
 
 #eval IsEven 9
 #eval IsOdd 9
+#eval IsEven 8
+#eval IsOdd 8
 
-example {n : ℕ} : IsOdd n = ((n%2) = 1) := by
-  apply iff_iff_eq.mp
+example {n : ℕ} : IsOdd n ↔ ((n%2) = 1) := by
   constructor
   -- <;>
   · intro h
diff --git a/references.md b/references.md
new file mode 100644
index 0000000..6491bdb
--- /dev/null
+++ b/references.md
@@ -0,0 +1,6 @@
+# References
+
+1. [Mathematics in Lean by Patrick Mossad and Jeremy Avigad](https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf)
+2. [The Mathlib 4 API docs](https://leanprover-community.github.io/mathlib4_docs/)
+3. [The Lean Zulip Chat](https://leanprover.zulipchat.com/)
+