# Overview All LeanNote files include this header template, which is customized to describe a particular file: ![[Topics/LeanNotes coding style/zResources/File header boilerplate-1.png]] Here is the source code: ```Lean /-! # URL: This url links to annotations, copyright, authors, and a README section. [URL goes here] # Summary: This docstring explains the purpose of the code in this file. It must be placed immediately after the imports. -/ ``` Code that requires acknowledge of prior copyright notices have a header that includes two sections for the: - copyright and author credits - a Read Me First section that provides a link to the file annotations. The file header boilerplate code has three sections that are specific to each *.lean* file: - **Copyright notice** : If the *.lean* file is a modification of a previously copyrighted work, then the previous copyright notice needs to be retained in full. Otherwise the [[LeanNotes copyright license]] can be used, which designates the software as a free and unencumbered piece of work that is released into the public domain. - **List of authors, including AI** : This comma separated list includes all authors that have made a significant contribution to this *.lean* file, including the AI tutors. - **Read Me First** : This section provides a link to the LeanNotes wiki page that annotates the *.lean* file: # Example headers ## Derived work Here is a snapshot of a header boilerplate from a file, *Sheet-1.lean,* that is derived from the eBook, [[Formalising Mathematics - Metha]]: ![[Appendix/Media/Images/Miscellaneous images/File header boilerplate-1.png]] Note that the LeanNotes wiki page that annotates this file has the same name as the file being annotated, [[Sheet 1 - LeanNotes Solutions]] ## Original work Here is an example of a header boilerplate with no previous copyright and only two authors: ```lean /- # Copyright and author credits Copyright (c) 2026, Den Ducoff. No rights reserved. Please refer to https://unlicense.org Authors: Den Ducoff, Gemini 3.5 # Read Me First A list of the tactics used in this file are available in LeanNotes wiki page: <LeanNotes wiki page url> -/ ``` --- Author: [[dducoff]] Posted Date: 2026-06-26