diff --git a/README.md b/README.md
index 43acafc..e790b42 100644
--- a/README.md
+++ b/README.md
@@ -2,6 +2,6 @@
 
 Formalizing local properties of modules in LEAN
 
-We will follow the [Stacks Project, Section 00EN](https://stacks.math.columbia.edu/tag/00EN).
+We will follow the Stacks Project, [Section 00EN](https://stacks.math.columbia.edu/tag/00EN), [Lemma 00HT](https://stacks.math.columbia.edu/tag/00HT), [Lemma 034K](https://stacks.math.columbia.edu/tag/034k), [Lemma 02JL](https://stacks.math.columbia.edu/tag/02JL), [Lemma 00GY](https://stacks.math.columbia.edu/tag/00GY).
 
-For API documentation, please visit https://mbkybky.github.io/module_localProperties/.
\ No newline at end of file
+For API documentation, please visit https://mbkybky.github.io/module_localProperties.