Mathematics in Lean
1. Introduction
2. Basics
3. Logic
4. Sets and Functions
5. Elementary Number Theory
6. Discrete Mathematics
7. Structures
8. Hierarchies
9. Groups and Rings
10. Linear algebra
11. Topology
12. Differential Calculus
13. Integration and Measure Theory
Index
Mathematics in Lean
Mathematics in Lean
View page source
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. Discrete Mathematics
6.1. More Induction
6.2. Finsets and Fintypes
6.3. Counting Arguments
6.4. 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