Mathematics in Lean

• 1. Introduction
  • 1.1. Getting Started
  • 1.2. Overview
• 2. Basics
  • 2.1. Calculating
  • 2.2. Proving Identities in Algebraic Structures
  • 2.3. Using Theorems and Lemmas
  • 2.4. More examples using apply and rw
  • 2.5. Proving Facts about Algebraic Structures
• 3. Logic
  • 3.1. Implication and the Universal Quantifier
  • 3.2. The Existential Quantifier
  • 3.3. Negation
  • 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. Topology
  • 9.1. Filters
  • 9.2. Metric spaces
  • 9.3. Topological spaces
• 10. Differential Calculus
  • 10.1. Elementary Differential Calculus
  • 10.2. Differential Calculus in Normed Spaces
• 11. Integration and Measure Theory
  • 11.1. Elementary Integration
  • 11.2. Measure Theory
  • 11.3. Integration