Mathematics in Lean

• 1. 引言
  • 1.1. 入门指南
  • 1.2. 概述
• 2. 基础知识
  • 2.1. 计算
  • 2.2. 证明代数结构中的恒等式
  • 2.3. 使用定理和引理
  • 2.4. 更多使用 apply 和 rw 的示例
  • 2.5. 证明关于代数结构的事实
• 3. 逻辑
  • 3.1. 蕴含和全称量词
  • 3.2. 存在量词
  • 3.3. 否定
  • 3.4. 合取和等价
  • 3.5. 析取
  • 3.6. 序列和收敛
• 4. 集合和函数
  • 4.1. 集合
  • 4.2. 函数
  • 4.3. 施罗德-伯恩斯坦定理
• 5. 初等数论
  • 5.1. 无理根
  • 5.2. 归纳和递归
  • 5.3. 素数无穷
  • 5.4. More Induction
• 6. Discrete Mathematics
  • 6.1. Finsets and Fintypes
  • 6.2. Counting Arguments
  • 6.3. Inductively Defined Types
• 7. Structures
  • 7.1. Defining structures
  • 7.2. Algebraic Structures
  • 7.3. Building the Gaussian Integers
• 8. Hierarchies
  • 8.1. Basics
  • 8.2. Morphisms
  • 8.3. Sub-objects
• 9. Groups and Rings
  • 9.1. Monoids and Groups
  • 9.2. Rings
• 10. Linear algebra
  • 10.1. Vector spaces and linear maps
  • 10.2. Subspaces and quotients
  • 10.3. Endomorphisms
  • 10.4. Matrices, bases and dimension
• 11. Topology
  • 11.1. Filters
  • 11.2. Metric spaces
  • 11.3. Topological spaces
• 12. Differential Calculus
  • 12.1. Elementary Differential Calculus
  • 12.2. Differential Calculus in Normed Spaces
• 13. Integration and Measure Theory
  • 13.1. Elementary Integration
  • 13.2. Measure Theory
  • 13.3. Integration