Local properties of modules Formalizing local properties of modules in LEAN We will follow the Stacks Project, Section 00EN, Lemma 00HT, Lemma 034K, Lemma 02JL, Lemma 00GY. For API documentation, please visit https://mbkybky.github.io/module_localProperties.