Home

Notes

• We maybe need a show more! button to go through big examples. Maybe we can use this: https://www.sphinx-doc.org/en/master/usage/restructuredtext/directives.html#directive-literalinclude.

• We need a mechanism for generating stable tags for exercises.

• The draft site is here.

• Patrick's tutorial is here.

• Kevin's Lagrange gist is here, Jeremy's follow up is here.

• Kevin's propositional exercises are here

• A glossary and a cheat sheet like this one will be helpful.

Ideas for a table of contents

• Introduction: done

• Basics: done

• Logic: done

• Set Theory

  • sets, functions, relations, big unions, images, etc.
  • example: least upper bounds and greatest lower bounds in a complete lattice, and on the reals
  • inverses and choice
  • quotients, e.g. quotienting a pre-order to get an order
  • Cantor-Bernstein

• Algebra

  • maybe the construction of the complex numbers?
  • some elementary group theory?
  • some specific groups, like the dihedral group?
  • Lagrange (and Euler-Fermat as a corollary)?
  • Cauchy's theorem (if p divides o(G), then G has an element of order p)?
  • First isomorphism theorem?
  • Sensitivity conjecture?
  • linear algebra?
  • Hilbert Basis Theorem?
  • lattices and Galois connections

• Topology

  • filters
  • topological spaces and metric spaces (with a pinch of uniform spaces). The forgetful inheritance pattern
  • big example: IVT

• Calculus

  • derivatives
  • integrals
  • find some nice example that brings everything together

• Discrete Mathematics

  • finite sets and cardinality
  • finite sums and products
  • maybe discrete probability, inclusion-exclusion?
  • Fibonacci numbers (can deal with casts to the complex numbers)

Skills to convey

(These are some things we should remember to tell readers about.)

• The simplifier
• Other automation (cc, etc.)
• Casting, norm_cast, etc.

Previous table of contents

Basic skills

• equational reasoning
• universal quantifiers and implication
• conjunction and negation
• disjunctions
• existential quantifiers

Fundamentals

• sets (union, Union, sUnion, bUnion...)
• relations (order relations and equivalence relations)
• functions (injective / surjective, inverses, etc.)
• finite sets and cardinality (a bit of combinatorics with finsets)
• the finite (Cantor Bernstein)

Numbers

• proof by induction
• there exist infinitely many primes
• integers, rationals, and reals
• fighting coercion hell; test case: proving that 1/(n+1) tends to zero (with home brewed limit definition, no filters).

Other ideas: Fibonacci numbers, Catalan numbers, binomial coefficients, irrationality of sqrt 2, sums of four squares, congruences.

Algebra

• some elementary group theory
• some specific groups, like the dihedral group?
• Lagrange (and Euler-Fermat as a corollary)?
• Cauchy's theorem (if p divides o(G), then G has an element of order p)?
• First isomorphism theorem?
• Sensitivity conjecture?
• linear algebra?
• lattices and Galois connections

Give background on declaring a structure and extending structures, using notation like * and <.

This is crucial because it is a huge barrier to using mathlib. You cannot do subgroups, ideals, or any topology or analysis without lattices. Galois connections are less necessary to use those theories, but they are crucial for anyone who wants to get even a tiny bit of understanding of how things are set up.

Topology

• filters
• topological spaces and metric spaces (with a pinch of uniform spaces). The forgetful inheritance pattern
• big example: IVT

Calculus

• derivatives
• integrals
• find some nice example that brings everything together