This is a supplementary note for MA3064 at University College Cork in 2026. It collects the main definitions and theorems covered in the course.

The source for this note is available on GitHub.

As an experiment, this note is accompanied by proofs written in Lean, a proof assistant and programming language for formal mathematics. Such tools are likely to become increasingly important in the future of mathematics. Students are not expected to read these proofs directly. However, if you would like to see the details of a proof, you might try copying a piece of Lean code and pasting it into your preferred AI agent with a prompt such as, "Please translate this into natural language."

Some definitions are borrowed from Mathlib, the mathematical library for Lean. Even when a concept is first introduced here using a definition given in this note, it may later be replaced by the corresponding Mathlib definition in order to use a more refined API.