Update Fri Apr 12 19:47:09 EDT 2024

Author: hrmacbeth

Math2001/Homework/hw8.lean

@@ -0,0 +1,21 @@
+/- Copyright (c) Heather Macbeth, 2024.  All rights reserved. -/
+import Mathlib.Tactic.GCongr
+import Library.Basic
+import AutograderLib
+
+math2001_init
+
+/-! # Homework 8
+
+Don't forget to compare with the text version,
+https://github.com/hrmacbeth/math2001/wiki/Homework-8,
+for clearer statements and any special instructions. -/
+
+
+@[autograded 4]
+theorem problem3 (m : ℤ) (hn : 66 ∣ 41 * m) : 66 ∣ m := by
+  sorry
+
+@[autograded 6]
+theorem problem4 (a : ℤ) : 3333 ∣ a ↔ (101 ∣ a ∧ 33 ∣ a) := by
+  sorry