lftcm2020:好奇数学家2020精益 源码

2020年好奇数学家精益课程 该资料库托管了2020年7月举行会议”的精益演示和练习 本次会议的教程记录。 (该存储库还托管会议网站,但是您可以忽略它。) 布局 在src文件夹中,您将找到许多包含精益文件的子目录: for_mathlib包含一些您可以忽略的背景材料。 demos包含一些在类别理论和线性代数教程中使用的文件。 exercise_sources包含按天组织的与每个教程相对应的练习。 hints包含有关这些练习的一些有用提示。 solutions包含完整的练习,如果您感到困惑并想窥视。 入门 我们强烈建议您使用支持工具leanproject精益leanproject 。 然后,您可以运行以下命令获取该项目并在VSCode中将其打开: leanproject get lftcm2020 cp -r lftcm2020/src/exercises_sources/ l