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/) +