Appendix B - Libraries

Packaging your own lemmas and theorems into a library is a tidier way of maintaining them, and making them available for others to use.

Library

In your project's lakefile.lean file, add a reference to the Lean file which contains your lemmas. 

lean_lib MyLeanLemmas

Replace MyLeanLemmas with the name you want for your own library.

Using A Library

To use the lemmas in the MyLeanLemmas library, we simply use import at the top of our lean program.

import Mathlib.Tactic

import MyLeanLemmas

It is a good habit to import additional libraries after any official Mathlib libraries.