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. Conjunction and Iff
  • 3.5. Disjunction
  • 3.6. Sequences and Convergence
• 4. Sets and Functions
  • 4.1. Sets
  • 4.2. Functions
  • 4.3. The Schröder-Bernstein Theorem
• 5. Elementary Number Theory
  • 5.1. Irrational Roots
  • 5.2. Induction and Recursion
  • 5.3. Infinitely Many Primes
• 6. Structures
  • 6.1. Defining structures
  • 6.2. Algebraic Structures
  • 6.3. Building the Gaussian Integers
• 7. Hierarchies
  • 7.1. Basics
  • 7.2. Morphisms
  • 7.3. Sub-objects
• 8. Groups and Rings
  • 8.1. Monoids and Groups
  • 8.2. Rings
• 9. Linear algebra
  • 9.1. Vector spaces and linear maps
  • 9.2. Subspaces and quotients
  • 9.3. Endomorphisms
  • 9.4. Matrices, bases and dimension
• 10. Topology
  • 10.1. Filters
  • 10.2. Metric spaces
  • 10.3. Topological spaces
• 11. Differential Calculus
  • 11.1. Elementary Differential Calculus
  • 11.2. Differential Calculus in Normed Spaces
• 12. Integration and Measure Theory
  • 12.1. Elementary Integration
  • 12.2. Measure Theory
  • 12.3. Integration