15. Number fields🔗

This page explains how to express the basic objects of algebraic number theory using the definitions in Mathlib: number fields, their rings of integers, ideals, units, the class group and the discriminant. We assume familiarity with both Lean and a first course in algebraic number theory, at the level of Marcus' Number Fields.

1. 15.1. Number fields
2. 15.2. The ring of integers
3. 15.3. Ideals
4. 15.4. The discriminant
5. 15.5. Units
6. 15.6. The class group