これは UCC の 2026 年の MA3064 の補足資料であり、授業で用いる定義と定理をまとめたものです。

この資料のソースは GitHub で公開しています。

試験的に、この資料には Lean で書かれた証明をつけています。 Lean は数学を厳密に記述するための proof assistant 兼 programming language です。 このような道具は今後ますます重要になると考えられています。 ただし、受講生に Lean で書かれた証明をそのまま読むことを求めるものではありません。 ですが、証明の詳細を知りたいときは Lean code をコピーして好きな AI エージェントに 「これを自然言語に翻訳してください」と頼んでみるのがよいと思います。

定義の一部は Lean の数学ライブラリである Mathlib から拝借しています。 また、ある節では自前で定義を与えていても、後の節ではより洗練された API を用いるために、対応する Mathlib の定義に置き換えることがあります。