Preliminaries (MA4N1/L01_polynomials.lean)
Generalizations, automation, exact?, simp, tactics (MA4N1/L02_generalizations.lean)
Groups (MA4N1/L03_groups.lean)
Developing an "API" around new definitions (MA4N1/L04_definitions.lean)
Graphs in Mathlib (MA4N1/L05_graphs.lean)
Continuity in Mathlib (MA4N1/L05_limits.lean)
Definitions, Structures and Typeclasses (MA4N1/L06_typeclasses.lean)
Performing calculations in Lean (MA4N1/L07_calculations.lean)
Defining the complex numbers (MA4N1/L08_Ri_hard.lean)
A short introduction to noncomputable and Decidable (MA4N1/L09_noncomputable_IsSquare.lean)
Divisibility as an excuse to see more tactics (MA4N1/L10_dvd_induction.lean)
Setting autoImplicit true or false (MA4N1/L11_autoImplicits.lean)
Pathologies (MA4N1/L12_pathologies.lean)
Pathologies of deriv (MA4N1/L13_deriv_pathologies.lean)
The in modifier (MA4N1/L14_in_implicit_explicit.lean)
Setoids and equivalence relations (MA4N1/L15_setoids.lean)
Finding lemmas in Mathlib (MA4N1/L17_navigating_Mathlib.lean)
Finiteness in Mathlib (MA4N1/L18_finiteness.lean)
Matrices in Lean (MA4N1/Matrices.lean)