More rings. Add group exercises

avigad · Oct 10, 2023 · 941a6bb · 941a6bb
1 parent 7ac9175
commit 941a6bb
Show file tree

Hide file tree

Showing 6 changed files with 473 additions and 111 deletions.
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -18,5 +18,22 @@
   "cSpell.words": [
     "monoids",
     "numref"
-  ]
+  ],
+  "spellright.language": [
+    "en_US"
+  ],
+  "spellright.documentTypes": [
+    "markdown",
+    "latex",
+    "plaintext",
+    "lean4"
+  ],
+  "spellright.parserByClass": {
+    "lean4": {
+      "parser": "code",
+      "comment_start": "/-",
+      "comment_end": "-/",
+      "comment_line": "--"
+    }
+  }
 }
diff --git a/MIL.lean b/MIL.lean
@@ -24,6 +24,7 @@ import MIL.C07_Hierarchies.S01_Basics
 import MIL.C07_Hierarchies.S02_Morphisms
 import MIL.C07_Hierarchies.S03_Subobjects
 import MIL.C08_Groups_and_Rings.S01_Groups
+import MIL.C08_Groups_and_Rings.S02_Rings
 import MIL.C10_Topology.S01_Filters
 import MIL.C10_Topology.S02_Metric_Spaces
 import MIL.C10_Topology.S03_Topological_Spaces