D110 · Mathematics in Lean · Study and teaching plans
Choose sections, code blocks and exercises. Save a plan with its original IDs and solution relationships intact.
13 chapters · 43 sections · 243 exercise-marked units
All readings — also works without JavaScript
- Getting Started
- Overview
- Calculating
- Proving Identities in Algebraic Structures
- Using Theorems and Lemmas
- More examples using apply and rw
- Proving Facts about Algebraic Structures
- Implication and the Universal Quantifier
- The Existential Quantifier
- Negation
- Conjunction and Iff
- Disjunction
- Sequences and Convergence
- Sets
- Functions
- The Schröder-Bernstein Theorem
- Irrational Roots
- Induction and Recursion
- Infinitely Many Primes
- More Induction
- Finsets and Fintypes
- Counting Arguments
- Inductively Defined Types
- Defining structures
- Algebraic Structures
- Building the Gaussian Integers
- Basics
- Morphisms
- Sub-objects
- Monoids and Groups
- Rings
- Vector spaces and linear maps
- Subspaces and quotients
- Endomorphisms
- Matrices, bases and dimension
- Filters
- Metric spaces
- Topological spaces
- Elementary Differential Calculus
- Differential Calculus in Normed Spaces
- Elementary Integration
- Measure Theory
- Integration
Build your selection
Scope and limits
- Indonesian and English interfaces, reading contexts and original code snippets are available. This is not an everyday-English rewrite.
- The English reader uses a different revision. Chapter/section links give reading context, not proof of equivalence for each code declaration.
- 243 units carry the native exercise flag; some are teaching examples. Six have no recorded solution relation.
- Solutions may fill one proof hole or give an alternative. Solution counts are not counts of completed exercises.
- An exercise snippet may be a shared block for several IDs. Source line numbers are not translated-file line numbers.
- Plans contain selections, provenance and links, not a complete offline book. No Lean code is executed.
Code: Apache-2.0; book text: CC BY 4.0. Original component notices are retained.
Data and source records · Structural validation